preStoneCech_hom_ext — Mathlib

English

If g1 and g2 are continuous and equal on preStoneCechUnit, then g1 = g2.

Русский

Если g1 и g2 непрерывны и равны на preStoneCechUnit, то g1 = g2.

LaTeX

$$∀{g₁,g₂}, Continuous g₁ → Continuous g₂ → g₁ ∘ preStoneCechUnit = g₂ ∘ preStoneCechUnit → g₁ = g₂$$

Lean4

theorem preStoneCech_hom_ext {g₁ g₂ : PreStoneCech α → β} (h₁ : Continuous g₁) (h₂ : Continuous g₂)
    (h : g₁ ∘ preStoneCechUnit = g₂ ∘ preStoneCechUnit) : g₁ = g₂ :=
  by
  apply Continuous.ext_on denseRange_preStoneCechUnit h₁ h₂
  rintro x ⟨x, rfl⟩
  apply congr_fun h x

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