Closure

📁 Source: Mathlib/Topology/Closure.lean

Statistics

Metric	Count
Definitions	0
Theorems closure, closure_eq, exists_mem_open, induction, inter_open_nonempty, interior_compl, mono, nonempty, nonempty_iff, of_closure, of_comp, closure_left, closure_right, frontier_left, frontier_right, lift'_closure, lift'_closure_eq_self, lift'_interior, lift'_interior_eq_self, le_lift'_closure, lift'_closure_eq_bot, lift'_interior_le, closure_biUnion, interior_iInter, closure_eq, closure_interior_subset, closure_subset, closure_subset_iff, frontier_eq, frontier_subset, mem_iff_closure_subset, frontier_eq, inter_frontier_eq, interior_eq, subset_interior_closure, subset_interior_iff, closure_biUnion, closure_sUnion, interior_biInter, interior_sInter, closure, of_closure, closure_closure, closure_compl, closure_diff_frontier, closure_diff_interior, closure_empty, closure_empty_iff, closure_eq_compl_interior_compl, closure_eq_iff_isClosed, closure_eq_interior_union_frontier, closure_eq_self_union_frontier, closure_iUnion_of_finite, closure_iUnion₂_le_nat, closure_iUnion₂_lt_nat, closure_inter_of_codisjoint_interior, closure_inter_open_nonempty_iff, closure_inter_subset, closure_inter_subset_inter_closure, closure_interior_idem, closure_minimal, closure_mono, closure_nonempty_iff, closure_subset_iff_isClosed, closure_union, closure_univ, compl_frontier_eq_union_interior, dense_closure, dense_compl_singleton_iff_not_open, dense_iff_closure_eq, dense_iff_inter_open, dense_univ, diff_subset_closure_iff, disjoint_frontier_iff_isOpen, disjoint_interior_frontier, exists_isClosed_iff, exists_isOpen_iff, forall_isClosed_iff, forall_isOpen_iff, frontier_closure_subset, frontier_compl, frontier_empty, frontier_eq_closure_inter_closure, frontier_eq_inter_compl_interior, frontier_inter_subset, frontier_interior_subset, frontier_subset_closure, frontier_subset_iff_isClosed, frontier_union_subset, frontier_univ, interior_closure_idem, interior_compl, interior_empty, interior_eq_compl_closure_compl, interior_eq_empty_iff_dense_compl, interior_eq_iff_isOpen, interior_eq_univ, interior_frontier, interior_iInter_of_finite, interior_iInter_subset, interior_iInter₂_le_nat, interior_iInter₂_lt_nat, interior_iInter₂_subset, interior_inter, interior_interior, interior_maximal, interior_mono, interior_sInter_subset, interior_subset, interior_subset_closure, interior_subset_iff, interior_union_inter_interior_compl_left_subset, interior_union_inter_interior_compl_right_subset, interior_union_isClosed_of_interior_empty, interior_union_of_disjoint_closure, interior_univ, isClosed_closure, isClosed_frontier, isClosed_of_closure_subset, isOpen_iff_forall_mem_open, isOpen_interior, mem_closure_iff, mem_interior, monotone_closure, notMem_of_notMem_closure, self_diff_frontier, subset_closure, subset_closure_inter_union_closure_compl_left, subset_closure_inter_union_closure_compl_right, subset_interior_iff, subset_interior_iff_isOpen, subset_interior_union	132
Total	132

Dense

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure 📖	mathematical	Dense	closure	—	dense_closure
closure_eq 📖	mathematical	Dense	closure Set.univ	—	dense_iff_closure_eq
exists_mem_open 📖	mathematical	Dense IsOpen Set.Nonempty	Set Set.instMembership	—	inter_open_nonempty
induction 📖	—	Dense	—	—	HasSubset.Subset.trans Set.instIsTransSubset Eq.subset Set.instReflSubset closure_eq IsClosed.closure_subset_iff Set.mem_univ
inter_open_nonempty 📖	mathematical	Dense IsOpen Set.Nonempty	Set Set.instInter	—	dense_iff_inter_open
interior_compl 📖	mathematical	Dense	interior Compl.compl Set Set.instCompl Set.instEmptyCollection	—	interior_eq_empty_iff_dense_compl compl_compl
mono 📖	—	Set Set.instHasSubset Dense	—	—	closure_mono
nonempty 📖	mathematical	Dense	Set.Nonempty	—	nonempty_iff
nonempty_iff 📖	mathematical	Dense	Set.Nonempty	—	inter_open_nonempty isOpen_univ
of_closure 📖	—	Dense closure	—	—	dense_closure

DenseRange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_comp 📖	—	DenseRange	—	—	Dense.mono Set.range_comp_subset_range

Disjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_left 📖	mathematical	Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice IsOpen	closure	—	mono_left closure_minimal subset_compl_right IsOpen.isClosed_compl disjoint_compl_left
closure_right 📖	mathematical	Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice IsOpen	closure	—	symm closure_left
frontier_left 📖	mathematical	IsOpen Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	frontier	—	Set.subset_compl_iff_disjoint_right HasSubset.Subset.trans Set.instIsTransSubset frontier_subset_closure closure_minimal Set.disjoint_left isClosed_compl_iff
frontier_right 📖	mathematical	IsOpen Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	frontier	—	symm frontier_left

Filter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_lift'_closure 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder lift' closure	—	le_lift' mem_of_superset subset_closure
lift'_closure_eq_bot 📖	mathematical	—	lift' closure Bot.bot Filter instBot	—	bot_unique le_lift'_closure lift'_bot monotone_closure closure_empty principal_empty
lift'_interior_le 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder lift' interior	—	mem_of_superset mem_lift' interior_subset

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lift'_closure 📖	mathematical	Filter.HasBasis	Filter.lift' closure	—	lift' monotone_closure
lift'_closure_eq_self 📖	mathematical	Filter.HasBasis IsClosed	Filter.lift' closure	—	le_antisymm ge_iff Filter.mem_lift' mem_of_mem IsClosed.closure_eq Filter.le_lift'_closure
lift'_interior 📖	mathematical	Filter.HasBasis	Filter.lift' interior	—	lift' interior_mono
lift'_interior_eq_self 📖	mathematical	Filter.HasBasis IsOpen	Filter.lift' interior	—	le_antisymm Filter.lift'_interior_le ge_iff lift'_interior IsOpen.interior_eq mem_of_mem

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_biUnion 📖	mathematical	—	closure Set.iUnion Finset instMembership	—	Set.Finite.closure_biUnion finite_toSet
interior_iInter 📖	mathematical	—	interior Set.iInter Finset instMembership	—	Set.Finite.interior_biInter finite_toSet

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_eq 📖	mathematical	—	closure	—	Set.Subset.antisymm closure_minimal Set.Subset.refl subset_closure
closure_interior_subset 📖	mathematical	—	Set Set.instHasSubset closure interior	—	closure_subset_iff interior_subset
closure_subset 📖	mathematical	—	Set Set.instHasSubset closure	—	closure_minimal Set.Subset.refl
closure_subset_iff 📖	mathematical	—	Set Set.instHasSubset closure	—	Set.Subset.trans subset_closure closure_minimal
frontier_eq 📖	mathematical	—	frontier Set Set.instSDiff interior	—	frontier.eq_1 closure_eq
frontier_subset 📖	mathematical	—	Set Set.instHasSubset frontier	—	frontier_subset_iff_isClosed
mem_iff_closure_subset 📖	mathematical	—	Set Set.instMembership Set.instHasSubset closure Set.instSingletonSet	—	closure_subset_iff Set.singleton_subset_iff

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
frontier_eq 📖	mathematical	IsOpen	frontier Set Set.instSDiff closure	—	frontier.eq_1 interior_eq
inter_frontier_eq 📖	mathematical	IsOpen	Set Set.instInter frontier Set.instEmptyCollection	—	frontier_eq Set.inter_diff_self
interior_eq 📖	mathematical	IsOpen	interior	—	HasSubset.Subset.antisymm Set.instAntisymmSubset interior_subset interior_maximal Set.Subset.refl
subset_interior_closure 📖	mathematical	IsOpen	Set Set.instHasSubset interior closure	—	subset_interior_iff subset_closure
subset_interior_iff 📖	mathematical	IsOpen	Set Set.instHasSubset interior	—	Set.Subset.trans interior_subset interior_maximal

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_biUnion 📖	mathematical	—	closure Set.iUnion Set Set.instMembership	—	closure_eq_compl_interior_compl Set.compl_iUnion interior_biInter Set.compl_iInter Set.iUnion_congr_Prop
closure_sUnion 📖	mathematical	—	closure Set.sUnion Set.iUnion Set Set.instMembership	—	Set.sUnion_eq_biUnion closure_biUnion
interior_biInter 📖	mathematical	—	interior Set.iInter Set Set.instMembership	—	induction_on Set.iInter_congr_Prop Set.iInter_of_empty instIsEmptyFalse Set.iInter_univ interior_univ Set.iInter_iInter_eq_or_left interior_inter
interior_sInter 📖	mathematical	—	interior Set.sInter Set.iInter Set Set.instMembership	—	Set.sInter_eq_biInter interior_biInter

Set.Nonempty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure 📖	mathematical	Set.Nonempty	closure	—	closure_nonempty_iff
of_closure 📖	—	Set.Nonempty closure	—	—	closure_nonempty_iff

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_closure 📖	mathematical	—	closure	—	IsClosed.closure_eq isClosed_closure
closure_compl 📖	mathematical	—	closure Compl.compl Set Set.instCompl interior	—	closure_eq_compl_interior_compl compl_compl
closure_diff_frontier 📖	mathematical	—	Set Set.instSDiff closure frontier interior	—	frontier.eq_1 Set.diff_diff_right_self Set.inter_eq_self_of_subset_right interior_subset_closure
closure_diff_interior 📖	mathematical	—	Set Set.instSDiff closure interior frontier	—	—
closure_empty 📖	mathematical	—	closure Set Set.instEmptyCollection	—	IsClosed.closure_eq isClosed_empty
closure_empty_iff 📖	mathematical	—	closure Set Set.instEmptyCollection	—	Set.subset_eq_empty subset_closure closure_empty
closure_eq_compl_interior_compl 📖	mathematical	—	closure Compl.compl Set Set.instCompl interior	—	interior.eq_1 closure.eq_1 Set.compl_sUnion Set.compl_image_set_of
closure_eq_iff_isClosed 📖	mathematical	—	closure IsClosed	—	isClosed_closure IsClosed.closure_eq
closure_eq_interior_union_frontier 📖	mathematical	—	closure Set Set.instUnion interior frontier	—	Set.union_diff_cancel interior_subset_closure
closure_eq_self_union_frontier 📖	mathematical	—	closure Set Set.instUnion frontier	—	Set.union_diff_cancel' interior_subset subset_closure
closure_iUnion_of_finite 📖	mathematical	—	closure Set.iUnion	—	Set.sUnion_range Set.Finite.closure_sUnion Set.finite_range Set.biUnion_range
closure_iUnion₂_le_nat 📖	mathematical	—	closure Set.iUnion	—	Set.Finite.closure_biUnion Set.finite_le_nat
closure_iUnion₂_lt_nat 📖	mathematical	—	closure Set.iUnion	—	Set.Finite.closure_biUnion Set.finite_lt_nat
closure_inter_of_codisjoint_interior 📖	mathematical	Codisjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instOrderTop interior	closure Set.instInter	—	compl_inj_iff Set.compl_inter interior_union_of_disjoint_closure closure_compl
closure_inter_open_nonempty_iff 📖	mathematical	IsOpen	Set.Nonempty Set Set.instInter closure	—	mem_closure_iff Set.inter_comm Set.Nonempty.mono inf_le_inf_right subset_closure
closure_inter_subset 📖	mathematical	—	Set Set.instHasSubset closure Set.instInter	—	Set.subset_inter closure_mono Set.inter_subset_left Set.inter_subset_right
closure_inter_subset_inter_closure 📖	mathematical	—	Set Set.instHasSubset closure Set.instInter	—	Monotone.map_inf_le monotone_closure
closure_interior_idem 📖	mathematical	—	closure interior	—	HasSubset.Subset.antisymm Set.instAntisymmSubset IsClosed.closure_interior_subset isClosed_closure closure_mono IsOpen.subset_interior_closure isOpen_interior
closure_minimal 📖	mathematical	Set Set.instHasSubset	closure	—	Set.sInter_subset_of_mem
closure_mono 📖	mathematical	Set Set.instHasSubset	closure	—	closure_minimal Set.Subset.trans subset_closure isClosed_closure
closure_nonempty_iff 📖	mathematical	—	Set.Nonempty closure	—	—
closure_subset_iff_isClosed 📖	mathematical	—	Set Set.instHasSubset closure IsClosed	—	isClosed_of_closure_subset IsClosed.closure_subset
closure_union 📖	mathematical	—	closure Set Set.instUnion	—	closure_eq_compl_interior_compl Set.compl_union interior_inter Set.compl_inter
closure_univ 📖	mathematical	—	closure Set.univ	—	IsClosed.closure_eq isClosed_univ
compl_frontier_eq_union_interior 📖	mathematical	—	Compl.compl Set Set.instCompl frontier Set.instUnion interior	—	frontier_eq_inter_compl_interior Set.compl_inter compl_compl
dense_closure 📖	mathematical	—	Dense closure	—	Dense.eq_1 closure_closure
dense_compl_singleton_iff_not_open 📖	mathematical	—	Dense Compl.compl Set Set.instCompl Set.instSingletonSet IsOpen	—	Set.Nonempty.ne_empty Dense.inter_open_nonempty Set.singleton_nonempty Set.inter_compl_self dense_iff_inter_open Set.inter_compl_nonempty_iff Set.eq_singleton_iff_nonempty_unique_mem
dense_iff_closure_eq 📖	mathematical	—	Dense closure Set.univ	—	Set.eq_univ_iff_forall
dense_iff_inter_open 📖	mathematical	—	Dense Set.Nonempty Set Set.instInter	—	mem_closure_iff
dense_univ 📖	mathematical	—	Dense Set.univ	—	subset_closure
diff_subset_closure_iff 📖	mathematical	—	Set Set.instHasSubset Set.instSDiff closure	—	Set.diff_subset_iff Set.union_eq_self_of_subset_left subset_closure
disjoint_frontier_iff_isOpen 📖	mathematical	—	Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice frontier IsOpen	—	isClosed_compl_iff frontier_subset_iff_isClosed frontier_compl Set.subset_compl_iff_disjoint_right
disjoint_interior_frontier 📖	mathematical	—	Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice interior frontier	—	Set.disjoint_iff_inter_eq_empty closure_diff_interior Set.diff_eq Set.inter_assoc Set.inter_comm Set.compl_inter_self Set.empty_inter
exists_isClosed_iff 📖	mathematical	—	IsClosed closure	—	IsClosed.closure_eq isClosed_closure
exists_isOpen_iff 📖	mathematical	—	IsOpen interior	—	IsOpen.interior_eq isOpen_interior
forall_isClosed_iff 📖	mathematical	—	closure	—	isClosed_closure IsClosed.closure_eq
forall_isOpen_iff 📖	mathematical	—	interior	—	isOpen_interior IsOpen.interior_eq
frontier_closure_subset 📖	mathematical	—	Set Set.instHasSubset frontier closure	—	Set.diff_subset_diff Eq.subset Set.instReflSubset closure_closure interior_mono subset_closure
frontier_compl 📖	mathematical	—	frontier Compl.compl Set Set.instCompl	—	frontier_eq_closure_inter_closure compl_compl Set.inter_comm
frontier_empty 📖	mathematical	—	frontier Set Set.instEmptyCollection	—	IsClosed.closure_eq interior_empty sdiff_self
frontier_eq_closure_inter_closure 📖	mathematical	—	frontier Set Set.instInter closure Compl.compl Set.instCompl	—	closure_compl frontier.eq_1 Set.diff_eq
frontier_eq_inter_compl_interior 📖	mathematical	—	frontier Set Set.instInter Compl.compl Set.instCompl interior	—	frontier_compl closure_compl Set.diff_eq closure_diff_interior
frontier_inter_subset 📖	mathematical	—	Set Set.instHasSubset frontier Set.instInter Set.instUnion closure	—	frontier_eq_closure_inter_closure Set.compl_inter closure_union LE.le.trans_eq Set.inter_subset_inter_left closure_inter_subset_inter_closure Set.inter_union_distrib_left Set.inter_assoc Set.inter_comm
frontier_interior_subset 📖	mathematical	—	Set Set.instHasSubset frontier interior	—	Set.diff_subset_diff closure_mono interior_subset Eq.subset Set.instReflSubset interior_interior
frontier_subset_closure 📖	mathematical	—	Set Set.instHasSubset frontier closure	—	Set.diff_subset
frontier_subset_iff_isClosed 📖	mathematical	—	Set Set.instHasSubset frontier IsClosed	—	frontier.eq_1 Set.diff_subset_iff Set.union_eq_right interior_subset closure_subset_iff_isClosed
frontier_union_subset 📖	mathematical	—	Set Set.instHasSubset frontier Set.instUnion Set.instInter closure Compl.compl Set.instCompl	—	frontier_compl frontier_inter_subset
frontier_univ 📖	mathematical	—	frontier Set.univ Set Set.instEmptyCollection	—	IsClosed.closure_eq interior_univ sdiff_self
interior_closure_idem 📖	mathematical	—	interior closure	—	HasSubset.Subset.antisymm Set.instAntisymmSubset interior_mono IsClosed.closure_interior_subset isClosed_closure IsOpen.subset_interior_closure isOpen_interior
interior_compl 📖	mathematical	—	interior Compl.compl Set Set.instCompl closure	—	closure_eq_compl_interior_compl compl_compl
interior_empty 📖	mathematical	—	interior Set Set.instEmptyCollection	—	IsOpen.interior_eq isOpen_empty
interior_eq_compl_closure_compl 📖	mathematical	—	interior Compl.compl Set Set.instCompl closure	—	closure_compl compl_compl
interior_eq_empty_iff_dense_compl 📖	mathematical	—	interior Set Set.instEmptyCollection Dense Compl.compl Set.instCompl	—	dense_iff_closure_eq closure_compl Set.compl_univ_iff
interior_eq_iff_isOpen 📖	mathematical	—	interior IsOpen	—	isOpen_interior IsOpen.interior_eq
interior_eq_univ 📖	mathematical	—	interior Set.univ	—	Set.univ_subset_iff Eq.trans_le interior_subset interior_univ
interior_frontier 📖	mathematical	—	interior frontier Set Set.instEmptyCollection	—	IsClosed.frontier_eq interior_mono Set.diff_subset interior_subset Set.subset_inter Set.subset_empty_iff Set.inter_diff_self
interior_iInter_of_finite 📖	mathematical	—	interior Set.iInter	—	Set.sInter_range Set.Finite.interior_sInter Set.finite_range Set.biInter_range
interior_iInter_subset 📖	mathematical	—	Set Set.instHasSubset interior Set.iInter	—	Set.subset_iInter interior_mono Set.iInter_subset
interior_iInter₂_le_nat 📖	mathematical	—	interior Set.iInter	—	Set.Finite.interior_biInter Set.finite_le_nat
interior_iInter₂_lt_nat 📖	mathematical	—	interior Set.iInter	—	Set.Finite.interior_biInter Set.finite_lt_nat
interior_iInter₂_subset 📖	mathematical	—	Set Set.instHasSubset interior Set.iInter	—	HasSubset.Subset.trans Set.instIsTransSubset interior_iInter_subset Set.iInter_mono
interior_inter 📖	mathematical	—	interior Set Set.instInter	—	LE.le.antisymm Monotone.map_inf_le interior_mono interior_maximal Set.inter_subset_inter interior_subset IsOpen.inter isOpen_interior
interior_interior 📖	mathematical	—	interior	—	IsOpen.interior_eq isOpen_interior
interior_maximal 📖	mathematical	Set Set.instHasSubset IsOpen	interior	—	Set.subset_sUnion_of_mem
interior_mono 📖	mathematical	Set Set.instHasSubset	interior	—	interior_maximal Set.Subset.trans interior_subset isOpen_interior
interior_sInter_subset 📖	mathematical	—	Set Set.instHasSubset interior Set.sInter Set.iInter Set.instMembership	—	Set.sInter_eq_biInter interior_iInter₂_subset
interior_subset 📖	mathematical	—	Set Set.instHasSubset interior	—	Set.sUnion_subset
interior_subset_closure 📖	mathematical	—	Set Set.instHasSubset interior closure	—	Set.Subset.trans interior_subset subset_closure
interior_subset_iff 📖	mathematical	—	Set Set.instHasSubset interior	—	—
interior_union_inter_interior_compl_left_subset 📖	mathematical	—	Set Set.instHasSubset Set.instInter interior Set.instUnion Compl.compl Set.instCompl	—	Eq.trans_subset interior_inter interior_mono Set.union_inter_compl_left_subset
interior_union_inter_interior_compl_right_subset 📖	mathematical	—	Set Set.instHasSubset Set.instInter interior Set.instUnion Compl.compl Set.instCompl	—	Eq.trans_subset interior_inter interior_mono Set.union_inter_compl_right_subset
interior_union_isClosed_of_interior_empty 📖	mathematical	interior Set Set.instEmptyCollection	Set.instUnion	—	by_contradiction IsOpen.subset_interior_iff IsOpen.sdiff Set.Subset.antisymm interior_maximal isOpen_interior interior_mono Set.subset_union_left
interior_union_of_disjoint_closure 📖	mathematical	Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice closure	interior Set.instUnion	—	interior_compl subset_antisymm Set.instAntisymmSubset Set.inter_univ Set.inter_union_distrib_left Set.union_subset HasSubset.Subset.trans Set.instIsTransSubset interior_union_inter_interior_compl_left_subset Set.subset_union_right interior_union_inter_interior_compl_right_subset Set.subset_union_left subset_interior_union
interior_univ 📖	mathematical	—	interior Set.univ	—	IsOpen.interior_eq isOpen_univ
isClosed_closure 📖	mathematical	—	IsClosed closure	—	isClosed_sInter
isClosed_frontier 📖	mathematical	—	IsClosed frontier	—	frontier_eq_closure_inter_closure IsClosed.inter isClosed_closure
isClosed_of_closure_subset 📖	mathematical	Set Set.instHasSubset closure	IsClosed	—	HasSubset.Subset.antisymm Set.instAntisymmSubset subset_closure isClosed_closure
isOpen_iff_forall_mem_open 📖	mathematical	—	IsOpen Set Set.instHasSubset Set.instMembership	—	subset_interior_iff_isOpen
isOpen_interior 📖	mathematical	—	IsOpen interior	—	isOpen_sUnion
mem_closure_iff 📖	mathematical	—	Set Set.instMembership closure Set.Nonempty Set.instInter	—	by_contradiction closure_minimal isClosed_compl_iff IsClosed.isOpen_compl
mem_interior 📖	mathematical	—	Set Set.instMembership interior Set.instHasSubset IsOpen	—	—
monotone_closure 📖	mathematical	—	Monotone Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra closure	—	closure_mono
notMem_of_notMem_closure 📖	—	Set Set.instMembership closure	—	—	subset_closure
self_diff_frontier 📖	mathematical	—	Set Set.instSDiff frontier interior	—	frontier.eq_1 Set.diff_diff_right Set.diff_eq_empty subset_closure Set.inter_eq_self_of_subset_right interior_subset Set.empty_union
subset_closure 📖	mathematical	—	Set Set.instHasSubset closure	—	Set.subset_sInter
subset_closure_inter_union_closure_compl_left 📖	mathematical	—	Set Set.instHasSubset closure Set.instUnion Set.instInter Compl.compl Set.instCompl	—	LE.le.trans_eq closure_mono Set.subset_inter_union_compl_left closure_union
subset_closure_inter_union_closure_compl_right 📖	mathematical	—	Set Set.instHasSubset closure Set.instUnion Set.instInter Compl.compl Set.instCompl	—	LE.le.trans_eq closure_mono Set.subset_inter_union_compl_right closure_union
subset_interior_iff 📖	mathematical	—	Set Set.instHasSubset interior IsOpen	—	isOpen_interior interior_subset HasSubset.Subset.trans Set.instIsTransSubset interior_maximal
subset_interior_iff_isOpen 📖	mathematical	—	Set Set.instHasSubset interior IsOpen	—	interior_eq_iff_isOpen
subset_interior_union 📖	mathematical	—	Set Set.instHasSubset Set.instUnion interior	—	Set.union_subset interior_mono Set.subset_union_left Set.subset_union_right

---

← Back to Index