compatible — Mathlib

English

If f is continuous, then a ≈ b implies f a = f b, with t2Setoid on X in scope.

Русский

Если f непрерывна, то a ≈ b значит f a = f b, когда в контексте задан t2Setoid X.

LaTeX

$$$ \\forall a\\,b:X,\\ a \\approx_{t2Setoid(X)} b \\Rightarrow f(a)=f(b)$$$

Lean4

theorem compatible {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} (hf : Continuous f) :
    letI _ := t2Setoid X
    ∀ (a b : X), a ≈ b → f a = f b :=
  by
  change t2Setoid X ≤ Setoid.ker f
  exact sInf_le <| .of_injective_continuous (Setoid.ker_lift_injective _) (hf.quotient_lift fun _ _ ↦ id)

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