Bases

Statistics

Metric	Count
Definitions	0
Theorems `eq_finite_iUnion_of_isTopologicalBasis_of_isCompact_open`, `eq_sUnion_finset_of_isTopologicalBasis_of_isCompact_open`, `isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis`	3
Total	3

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_finite_iUnion_of_isTopologicalBasis_of_isCompact_open` 📖	mathematical	`TopologicalSpace.IsTopologicalBasis` `Set.range` `Set` `IsCompact` `IsOpen`	`Set.Finite` `Set.iUnion` `Set.instMembership`	—	`TopologicalSpace.IsTopologicalBasis.open_eq_iUnion` `IsCompact.elim_finite_subcover` `TopologicalSpace.IsTopologicalBasis.isOpen` `Set.mem_range_self` `subset_refl` `Set.instReflSubset` `Set.toFinite` `Finite.of_fintype` `le_antisymm` `Set.Subset.trans` `Set.iUnion_congr_Prop` `Finset.coe_image` `Set.iUnion_exists` `Set.biUnion_and'` `Set.iUnion_iUnion_eq_right` `Set.subset_iUnion₂` `Set.iUnion₂_subset` `Finset.mem_image` `Set.subset_iUnion`
`eq_sUnion_finset_of_isTopologicalBasis_of_isCompact_open` 📖	mathematical	`TopologicalSpace.IsTopologicalBasis` `IsCompact` `IsOpen`	`Set.sUnion` `Set.image` `Set` `Set.instMembership` `SetLike.coe` `Finset` `Set.Elem` `Finset.instSetLike`	—	`Subtype.range_coe_subtype` `Set.iUnion_coe_set` `Set.iUnion_congr_Prop` `Set.coe_toFinset` `Set.sUnion_image` `eq_finite_iUnion_of_isTopologicalBasis_of_isCompact_open`
`isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis` 📖	mathematical	`TopologicalSpace.IsTopologicalBasis` `Set.range` `Set` `IsCompact`	`IsOpen` `Set.Finite` `Set.iUnion` `Set.instMembership`	—	`eq_finite_iUnion_of_isTopologicalBasis_of_isCompact_open` `Set.Finite.isCompact_biUnion` `isOpen_biUnion` `TopologicalSpace.IsTopologicalBasis.isOpen` `Set.mem_range_self`

---