theorem
PiBase.lC1_of_homeomorph
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
(e : X ≃ₜ Y)
(h : LC1 X)
:
LC1 Y
LC¹ is transported along a homeomorphism.
Given y : Y and M ∈ 𝓝 y, pull M back to N = e ⁻¹' M ∈ 𝓝 (e.symm y) and let
eN : ↥N ≃ₜ ↥M be the induced homeomorphism. A witness U ⊆ ↥N for X transports to
eN.symm ⁻¹' U = eN '' U, whose inclusion into ↥M factors as
eN ∘ (U ↪ N) ∘ (eN.symm ⁻¹' U ≃ₜ U), so functoriality of FundamentalGroup.map kills it.
theorem
PiBase.Homeomorph.lC1
{X : Type u_1}
{Y : Type u_2}
[TopologicalSpace X]
[TopologicalSpace Y]
(f : X ≃ₜ Y)
[LC1 X]
:
LC1 Y