eq_if_stoneCechUnit_eq — Mathlib

English

If stoneCechUnit a = stoneCechUnit b, then f a = f b for any continuous f.

Русский

Если stoneCechUnit a = stoneCechUnit b, то f a = f b для любого непрерывного f.

LaTeX

$$$ stoneCechUnit a = stoneCechUnit b \Rightarrow f a = f b $$$

Lean4

theorem eq_if_stoneCechUnit_eq {a b : α} {f : α → β} (hcf : Continuous f) (h : stoneCechUnit a = stoneCechUnit b) :
    f a = f b :=
  by
  rw [← congrFun (stoneCechExtend_extends hcf), ← congrFun (stoneCechExtend_extends hcf)]
  exact congrArg (stoneCechExtend hcf) h

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