LocallyCompactRegular

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

Statistics

Metric	Count
Definitions	0
Theorems of_t2Space_locallyCompactSpace, of_t2Space_locallyCompactSpace	2
Total	2

BaireSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_t2Space_locallyCompactSpace 📖	mathematical	—	BaireSpace	—	dense_iff_inter_open IsOpen.exists_positiveCompacts_closure_subset IsOpen.inter isOpen_interior Set.inter_comm Dense.inter_open_nonempty TopologicalSpace.PositiveCompacts.interior_nonempty HasSubset.Subset.trans Set.instIsTransSubset subset_closure Set.inter_subset_right interior_subset Set.inter_subset_left IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed closure_mono Set.Nonempty.closure TopologicalSpace.PositiveCompacts.nonempty IsCompact.closure TopologicalSpace.PositiveCompacts.isCompact isClosed_closure Set.Nonempty.mono

IsGδ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_t2Space_locallyCompactSpace 📖	mathematical	IsGδ	BaireSpace Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	BaireSpace.of_t2Space_locallyCompactSpace instR1SpaceSubtype IsClosed.locallyCompactSpace isClosed_closure baireSpace_of_dense isGδ_induced continuous_subtype_val Subtype.image_preimage_coe Set.inter_eq_right subset_closure Set.instReflSubset Continuous.comp' Homeomorph.baireSpace

---

← Back to Index