eq_if_preStoneCechUnit_eq — Mathlib

English

If preStoneCechUnit a = preStoneCechUnit b, then g a = g b.

Русский

Если preStoneCechUnit a = preStoneCechUnit b, тогда g a = g b.

LaTeX

$$$ preStoneCechUnit a = preStoneCechUnit b \Rightarrow g a = g b $$$

Lean4

theorem eq_if_preStoneCechUnit_eq {a b : α} (h : preStoneCechUnit a = preStoneCechUnit b) : g a = g b :=
  by
  have e := ultrafilter_extend_extends g
  rw [← congrFun e a, ← congrFun e b, Function.comp_apply, Function.comp_apply]
  rw [preStoneCechUnit, preStoneCechUnit, Quot.eq] at h
  generalize (pure a : Ultrafilter α) = F at h
  generalize (pure b : Ultrafilter α) = G at h
  induction h with
  | rel x y a =>
    exact
      let ⟨a, hx, hy⟩ := a;
      preStoneCechCompat hg hx hy
  | refl x => rfl
  | symm x y _ h => rw [h]
  | trans x y z _ _ h h' => exact h.trans h'

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