ext_of_eq_adjoin — Mathlib

English

Same extensional principle for adjoin as above, asserted for generalized contexts.

Русский

Та же экстенсивность для adjoin как выше, в обобщённых условиях.

LaTeX

$$$\\text{ext}_{\\operatorname{adjoin}}(s)$$$

Lean4

theorem ext_of_eq_adjoin {S : Subalgebra R A} {s : Set A} (hS : S = adjoin R s) ⦃φ₁ φ₂ : S →ₐ[R] B⦄
    (h : ∀ x hx, φ₁ ⟨x, hS.ge (subset_adjoin hx)⟩ = φ₂ ⟨x, hS.ge (subset_adjoin hx)⟩) : φ₁ = φ₂ := by subst hS;
  exact adjoin_ext h

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