English
There is a uniform isomorphism obtained by pre-composing with a bijection e : γ ≃ α, provided certain 𝔗 ⊆ image e⁻¹ 𝔖 and 𝔖 ⊆ preimage e⁻¹ 𝔗.
Русский
Существует равномерная изоморфия, полученная до пред-композиции через биекция e: γ ≃ α, при условии 𝔗 ⊆ image e⁻¹ 𝔖 и 𝔖 ⊆ preimage e⁻¹ 𝔗.
LaTeX
$$UniformOnFun.congrLeft {𝔗} (e : γ ≃ α) (he : 𝔗 ⊆ image e ⁻¹' 𝔖) (he' : 𝔖 ⊆ preimage e ⁻¹' 𝔗) : (γ →ᵤ[𝔗] β) ≃ᵤ (α →ᵤ[𝔖] β).$$
Lean4
/-- Turn a bijection `e : γ ≃ α` such that we have both `∀ T ∈ 𝔗, e '' T ∈ 𝔖` and
`∀ S ∈ 𝔖, e ⁻¹' S ∈ 𝔗` into a uniform isomorphism `(γ →ᵤ[𝔗] β) ≃ᵤ (α →ᵤ[𝔖] β)` by pre-composing. -/
protected def congrLeft {𝔗 : Set (Set γ)} (e : γ ≃ α) (he : 𝔗 ⊆ image e ⁻¹' 𝔖) (he' : 𝔖 ⊆ preimage e ⁻¹' 𝔗) :
(γ →ᵤ[𝔗] β) ≃ᵤ (α →ᵤ[𝔖] β) :=
{
Equiv.arrowCongr e
(Equiv.refl
_) with
uniformContinuous_toFun :=
UniformOnFun.precomp_uniformContinuous fun s hs ↦
by
change e.symm '' s ∈ 𝔗
rw [← preimage_equiv_eq_image_symm]
exact he' hs
uniformContinuous_invFun := UniformOnFun.precomp_uniformContinuous he }
