Lemmas

📁 Source: Mathlib/Topology/Baire/Lemmas.lean

Statistics

Metric	Count
Definitions	0
Theorems inter_of_Gδ, baireSpace_of_dense, dense_biUnion_interior_of_closed, dense_iUnion_interior_of_closed, dense_sUnion_interior_of_closed, baireSpace, dense_sInter, baireSpace, baire_of_finite, dense_biInter_of_Gδ, dense_biInter_of_isOpen, dense_biUnion_interior_of_closed, dense_iInter_of_Gδ, dense_iInter_of_isOpen, dense_iInter_of_isOpen_nat, dense_iUnion_interior_of_closed, dense_of_mem_residual, dense_sInter_of_Gδ, dense_sInter_of_isOpen, dense_sUnion_interior_of_closed, eventually_residual, mem_residual, nonempty_interior_of_iUnion_of_closed, not_isMeagre_of_isGδ_of_dense, not_isMeagre_of_isOpen, not_isMeagre_of_mem_residual	26
Total	26

Dense

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inter_of_Gδ 📖	mathematical	IsGδ Dense	Set Set.instInter	—	Set.inter_eq_iInter dense_iInter_of_Gδ Bool.countable

IsGδ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baireSpace_of_dense 📖	mathematical	IsGδ Dense	BaireSpace Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	eq_iInter_nat BaireSpace.baire_property IsOpen.inter Dense.inter_of_isOpen_left Dense.mono Set.ext Subtype.dense_iff exists_open_dense_of_open_dense_subtype
dense_biUnion_interior_of_closed 📖	mathematical	IsGδ Dense IsClosed Set Set.instHasSubset Set.iUnion Set.instMembership	interior	—	Set.biUnion_eq_iUnion dense_iUnion_interior_of_closed Set.Countable.to_subtype
dense_iUnion_interior_of_closed 📖	mathematical	IsGδ Dense IsClosed Set Set.instHasSubset Set.iUnion	interior	—	IsClosed.isOpen_compl isClosed_frontier dense_iInter_of_isOpen closure_compl interior_frontier Dense.mono Set.mem_iUnion Set.mem_iInter self_diff_frontier Dense.inter_of_Gδ iInter_of_isOpen
dense_sUnion_interior_of_closed 📖	mathematical	IsGδ Dense IsClosed Set Set.instHasSubset Set.sUnion	Set.iUnion Set.instMembership interior	—	dense_biUnion_interior_of_closed Set.sUnion_eq_biUnion

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baireSpace 📖	mathematical	IsOpen	BaireSpace Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	Topology.IsOpenEmbedding.baireSpace isOpenEmbedding_subtypeVal

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dense_sInter 📖	mathematical	IsOpen Dense	Set.sInter	—	induction_on Set.sInter_empty Set.sInter_insert Dense.inter_of_isOpen_right isOpen_sInter

Topology.IsOpenEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baireSpace 📖	mathematical	Topology.IsOpenEmbedding	BaireSpace	—	IsOpen.union isOpenMap IsClosed.isOpen_compl isClosed_closure dense_iff_closure_eq subset_antisymm_iff Set.instReflSubset Set.instAntisymmSubset Set.union_subset_union interior_subset subset_refl closure_minimal Continuous.range_subset_closure_image_dense continuous closure_compl closure_union dense_iInter_of_isOpen_nat Set.ext Function.Injective.mem_set_image Topology.IsEmbedding.injective toIsEmbedding imp_iff_or_not subset_closure Set.mem_range_self Dense.preimage

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baire_of_finite 📖	mathematical	—	BaireSpace	—	Set.Finite.dense_sInter Set.toFinite Subtype.finite Set.instFinite Set.sInter_range
dense_biInter_of_Gδ 📖	mathematical	IsGδ Dense	Set.iInter Set Set.instMembership	—	Set.biInter_eq_iInter dense_iInter_of_Gδ Set.Countable.to_subtype
dense_biInter_of_isOpen 📖	mathematical	IsOpen Dense	Set.iInter Set Set.instMembership	—	Set.sInter_image dense_sInter_of_isOpen Set.forall_mem_image Set.Countable.image
dense_biUnion_interior_of_closed 📖	mathematical	IsClosed Set.iUnion Set Set.instMembership Set.univ	Dense interior	—	IsGδ.dense_biUnion_interior_of_closed IsGδ.univ dense_univ Eq.ge
dense_iInter_of_Gδ 📖	mathematical	IsGδ Dense	Set.iInter	—	dense_sInter_of_Gδ Set.forall_mem_range Set.countable_range
dense_iInter_of_isOpen 📖	mathematical	IsOpen Dense	Set.iInter	—	dense_sInter_of_isOpen Set.forall_mem_range Set.countable_range
dense_iInter_of_isOpen_nat 📖	mathematical	IsOpen Dense	Set.iInter	—	BaireSpace.baire_property
dense_iUnion_interior_of_closed 📖	mathematical	IsClosed Set.iUnion Set.univ	Dense interior	—	IsGδ.dense_iUnion_interior_of_closed IsGδ.univ dense_univ Eq.ge
dense_of_mem_residual 📖	mathematical	Set Filter Filter.instMembership residual	Dense	—	mem_residual Dense.mono
dense_sInter_of_Gδ 📖	mathematical	IsGδ Dense	Set.sInter	—	dense_of_mem_residual countable_sInter_mem countableInterFilter_residual residual_of_dense_Gδ
dense_sInter_of_isOpen 📖	mathematical	IsOpen Dense	Set.sInter	—	Set.eq_empty_or_nonempty Set.sInter_empty Set.Countable.exists_eq_range dense_iInter_of_isOpen_nat Set.forall_mem_range
dense_sUnion_interior_of_closed 📖	mathematical	IsClosed Set.sUnion Set.univ	Dense Set.iUnion Set Set.instMembership interior	—	IsGδ.dense_sUnion_interior_of_closed IsGδ.univ dense_univ Eq.ge
eventually_residual 📖	mathematical	—	Filter.Eventually residual IsGδ Dense	—	—
mem_residual 📖	mathematical	—	Set Filter Filter.instMembership residual Set.instHasSubset IsGδ Dense	—	mem_residual_iff dense_sInter_of_isOpen Filter.mem_of_superset residual_of_dense_Gδ
nonempty_interior_of_iUnion_of_closed 📖	mathematical	IsClosed Set.iUnion Set.univ	Set.Nonempty interior	—	Dense.nonempty dense_iUnion_interior_of_closed
not_isMeagre_of_isGδ_of_dense 📖	mathematical	IsGδ Dense	IsMeagre	—	mem_residual Dense.nonempty Dense.inter_of_Gδ
not_isMeagre_of_isOpen 📖	mathematical	IsOpen Set.Nonempty	IsMeagre	—	Dense.inter_open_nonempty dense_of_mem_residual IsMeagre.eq_1
not_isMeagre_of_mem_residual 📖	mathematical	Set Filter Filter.instMembership residual	IsMeagre	—	mem_residual not_isMeagre_of_isGδ_of_dense IsMeagre.mono

---

← Back to Index