CompHaus.is_hausdorff
theorem CompHaus.is_hausdorff : ∀ (self : CompHaus), T2Space ↑self.toTop
This theorem states that the underlying topological space of any compactly generated Hausdorff space (`CompHaus`) is a T2 space. In the realm of topology, a T2 space, also known as a Hausdorff space, is a particular type of topological space where any two distinct points can be separated by disjoint open sets. Therefore, this theorem is affirming the Hausdorff property for compactly generated Hausdorff spaces.
More concisely: Every compactly generated Hausdorff space is a T2 space.
|
CompHaus.is_compact
theorem CompHaus.is_compact : ∀ (self : CompHaus), CompactSpace ↑self.toTop
This theorem states that the underlying topological space of any compact Hausdorff space (denoted as `CompHaus` in Lean 4) is compact. In other words, given any compact Hausdorff space, the associated topology is compact, which means that every open cover of the space has a finite subcover.
More concisely: Every compact Hausdorff space is a topologically compact space.
|
CompHaus.isClosedMap
theorem CompHaus.isClosedMap : ∀ {X Y : CompHaus} (f : X ⟶ Y), IsClosedMap ⇑f
This theorem states that any continuous function operating on compact Hausdorff spaces is a closed map. In more detail, given any two compact Hausdorff spaces 'X' and 'Y', and any continuous function 'f' from 'X' to 'Y', the theorem guarantees that 'f' preserves the property of being closed. That is, the image under 'f' of any closed set in 'X' is a closed set in 'Y'.
More concisely: Any continuous function between compact Hausdorff spaces is a closed map, meaning the image of a closed set under such a function is closed.
|
CompHaus.epi_iff_surjective
theorem CompHaus.epi_iff_surjective : ∀ {X Y : CompHaus} (f : X ⟶ Y), CategoryTheory.Epi f ↔ Function.Surjective ⇑f
The theorem `CompHaus.epi_iff_surjective` states that for any two compact Hausdorff spaces `X` and `Y`, and a morphism `f` from `X` to `Y`, `f` is an epimorphism in the category of compact Hausdorff spaces if and only if the function represented by `f` is surjective. In other words, `f` is an epimorphism (i.e., splitting monomorphism or every parallel pair of morphisms `g, h : Y → Z` such that `g ∘ f = h ∘ f` implies `g = h`) if and only if for every element `b` in `Y`, there exists an element `a` in `X` such that `f(a) = b`.
More concisely: A morphism between compact Hausdorff spaces is an epimorphism if and only if it is surjective.
|
CompHaus.isIso_of_bijective
theorem CompHaus.isIso_of_bijective : ∀ {X Y : CompHaus} (f : X ⟶ Y), Function.Bijective ⇑f → CategoryTheory.IsIso f
The theorem `CompHaus.isIso_of_bijective` states that for any continuous bijection `f` between two compact Hausdorff spaces `X` and `Y`, `f` is an isomorphism. Here, a bijection is a function that is both injective (no two different inputs map to the same output) and surjective (every possible output is the result of some input). In other words, if we have a bijective continuous function between two compact Hausdorff spaces, then this function has an inverse that is also a continuous function, making it an isomorphism in the category of compact Hausdorff spaces.
More concisely: If `f` is a continuous bijection between two compact Hausdorff spaces, then `f` is an isomorphism (has a continuous inverse).
|