faithful — Mathlib

English

The functor compactumToCompHaus is faithful.

Русский

Функтор compactumToCompHaus верен (faithful).

LaTeX

$$$\\text{faithful}(\\text{compactumToCompHaus})$$$

Lean4

/-- The functor `compactumToCompHaus` is faithful. -/
instance faithful : compactumToCompHaus.Faithful where
  -- Porting note: this used to be obviously (though it consumed a bit of memory)
  map_injective := by
    intro _ _ _ _ h
    apply Monad.Algebra.Hom.ext
    apply congrArg (fun f => f.hom.toFun) h

Похожие утверждения