LocallyClosed

📁 Source: Mathlib/Topology/LocallyClosed.lean

Statistics

Metric	Count
Definitions	0
Theorems preimage_coborder_subset, coborder_eq, image, inter, isOpen_coborder, isOpen_preimage_val_closure, preimage, coborder_eq, coborder_preimage_subset, isLocallyClosed_iff, isLocallyClosed_iff, coborder_preimage, closure_inter_coborder, coborder_eq_compl_frontier_iff, coborder_eq_union_closure_compl, coborder_eq_union_frontier_compl, coborder_eq_univ_iff, coborder_inter_closure, coborder_preimage, dense_coborder, isClosed_preimage_val_coborder, isLocallyClosed_iff_isOpen_coborder, isLocallyClosed_tfae, subset_coborder	24
Total	24

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preimage_coborder_subset 📖	mathematical	Continuous	Set Set.instHasSubset Set.preimage coborder	—	coborder.eq_1 Set.preimage_compl Set.preimage_diff Set.compl_subset_compl Set.diff_subset_diff_left closure_preimage_subset

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coborder_eq 📖	mathematical	—	coborder Set.univ	—	coborder_eq_univ_iff

IsLocallyClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image 📖	mathematical	IsLocallyClosed Topology.IsInducing Set.range	Set.image	—	Topology.IsInducing.isLocallyClosed_iff Set.image_preimage_eq_inter_range inter
inter 📖	mathematical	IsLocallyClosed	Set Set.instInter	—	IsOpen.inter IsClosed.inter Set.inter_inter_inter_comm
isOpen_coborder 📖	mathematical	IsLocallyClosed	IsOpen coborder	—	isLocallyClosed_iff_isOpen_coborder
isOpen_preimage_val_closure 📖	mathematical	IsLocallyClosed	IsOpen Set.Elem closure instTopologicalSpaceSubtype Set Set.instMembership Set.preimage	—	List.TFAE.out isLocallyClosed_tfae
preimage 📖	mathematical	IsLocallyClosed Continuous	Set.preimage	—	IsOpen.preimage IsClosed.preimage Set.preimage_inter

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coborder_eq 📖	mathematical	IsOpen	coborder Compl.compl Set Set.instCompl frontier	—	coborder_eq_compl_frontier_iff

IsOpenMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coborder_preimage_subset 📖	mathematical	IsOpenMap	Set Set.instHasSubset coborder Set.preimage	—	coborder.eq_1 Set.preimage_compl Set.preimage_diff Set.compl_subset_compl Set.diff_subset_diff_left preimage_closure_subset_closure_preimage

Topology.IsEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocallyClosed_iff 📖	mathematical	Topology.IsEmbedding	IsLocallyClosed Set Set.instInter Set.range Set.image	—	Topology.IsInducing.isLocallyClosed_iff isInducing Set.image_injective injective Set.image_preimage_eq_inter_range

Topology.IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocallyClosed_iff 📖	mathematical	Topology.IsInducing	IsLocallyClosed Set.preimage	—	isOpen_iff isClosed_iff

Topology.IsOpenEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coborder_preimage 📖	mathematical	Topology.IsOpenEmbedding	coborder Set.preimage	—	coborder_preimage isOpenMap continuous

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_inter_coborder 📖	mathematical	—	Set Set.instInter closure coborder	—	Set.inter_comm coborder_inter_closure
coborder_eq_compl_frontier_iff 📖	mathematical	—	coborder Compl.compl Set Set.instCompl frontier IsOpen	—	coborder_eq_union_frontier_compl
coborder_eq_union_closure_compl 📖	mathematical	—	coborder Set Set.instUnion Compl.compl Set.instCompl closure	—	coborder.eq_1 compl_eq_comm Set.compl_union compl_compl Set.inter_comm
coborder_eq_union_frontier_compl 📖	mathematical	—	coborder Set Set.instUnion Compl.compl Set.instCompl frontier	—	coborder.eq_1 compl_eq_comm Set.compl_union compl_compl Set.diff_eq_compl_inter Set.union_diff_right Set.union_comm closure_eq_self_union_frontier
coborder_eq_univ_iff 📖	mathematical	—	coborder Set.univ IsClosed	—	—
coborder_inter_closure 📖	mathematical	—	Set Set.instInter coborder closure	—	coborder.eq_1 Set.diff_eq_compl_inter Set.diff_diff_right_self Set.inter_eq_right subset_closure
coborder_preimage 📖	mathematical	IsOpenMap Continuous	coborder Set.preimage	—	HasSubset.Subset.antisymm Set.instAntisymmSubset IsOpenMap.coborder_preimage_subset Continuous.preimage_coborder_subset
dense_coborder 📖	mathematical	—	Dense coborder	—	dense_iff_closure_eq coborder_eq_union_closure_compl closure_union Set.univ_subset_iff subset_trans Set.instIsTransSubset Set.union_compl_self Set.instReflSubset Set.union_subset_union_right subset_closure
isClosed_preimage_val_coborder 📖	mathematical	—	IsClosed Set.Elem coborder instTopologicalSpaceSubtype Set Set.instMembership Set.preimage	—	isClosed_preimage_val Set.inter_eq_right subset_coborder coborder_inter_closure subset_refl Set.instReflSubset
isLocallyClosed_iff_isOpen_coborder 📖	mathematical	—	IsLocallyClosed IsOpen coborder	—	List.TFAE.out isLocallyClosed_tfae
isLocallyClosed_tfae 📖	mathematical	—	List.TFAE IsLocallyClosed IsOpen coborder Set.Elem closure instTopologicalSpaceSubtype Set Set.instMembership Set.preimage	—	IsClosed.closure_eq Set.compl_subset_iff_union Set.compl_subset_compl HasSubset.Subset.trans Set.instIsTransSubset frontier_subset_closure closure_mono Set.inter_subset_right coborder_eq_union_frontier_compl Set.inter_union_distrib_right Set.inter_univ IsOpen.union IsClosed.isOpen_compl isClosed_frontier IsOpen.mem_nhds subset_coborder isClosed_preimage_val_coborder mem_nhds_iff Set.subset_inter Set.inter_subset_left IsOpen.inter_closure Set.inter_subset_inter subset_rfl Set.instReflSubset isClosed_preimage_val isOpen_iUnion Set.ext Set.subset_iUnion₂ Subtype.image_preimage_coe subset_closure IsLocallyClosed.image IsOpen.isLocallyClosed Topology.IsInducing.subtypeVal Subtype.range_coe_subtype IsClosed.isLocallyClosed isClosed_closure List.tfae_of_cycle
subset_coborder 📖	mathematical	—	Set Set.instHasSubset coborder	—	coborder.eq_1 Set.subset_compl_iff_disjoint_right disjoint_sdiff_self_right

---

← Back to Index