stoneCech_hom_ext — Mathlib

English

The universal property for maps g1,g2: StoneCech α → β: if h1,h2 are continuous and g1 ∘ stoneCechUnit = g2 ∘ stoneCechUnit, then g1 = g2.

Русский

Универсальное свойство для отображений g1,g2: StoneCech α → β: если g1,g2 непрерывны и g1 ∘ unit = g2 ∘ unit, то g1 = g2.

LaTeX

$$$ \forall g_1,g_2:\, StoneCech(\alpha) \to \beta,\; Continuous(g_1) \to Continuous(g_2) \to (g_1 \circ stoneCechUnit = g_2 \circ stoneCechUnit) \to g_1 = g_2 $$$

Lean4

theorem stoneCech_hom_ext {g₁ g₂ : StoneCech α → β} (h₁ : Continuous g₁) (h₂ : Continuous g₂)
    (h : g₁ ∘ stoneCechUnit = g₂ ∘ stoneCechUnit) : g₁ = g₂ :=
  by
  apply h₁.ext_on denseRange_stoneCechUnit h₂
  rintro _ ⟨x, rfl⟩
  exact congr_fun h x

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