eqOn_sup — Mathlib

English

If φ and ψ agree on S and on T as subalgebras, they agree on the supremum S ⊔ T.

Русский

Если φ и ψ согласны на подпалгебрах S и T, они согласны на наивысшую сумму S ⊔ T.

LaTeX

$$$ \\mathrm{eqOn\_sup} : \\mathrm{Set.EqOn}(\\varphi,\\psi) S \\rightarrow \\mathrm{Set.EqOn}(\\varphi,\\psi) T \\rightarrow \\mathrm{Set.EqOn}(\\varphi,\\psi) (S \\,\\oplus\\, T) $$$

Lean4

theorem eqOn_sup {φ ψ : F} {S T : Subalgebra R A} (hS : Set.EqOn φ ψ S) (hT : Set.EqOn φ ψ T) : Set.EqOn φ ψ ↑(S ⊔ T) :=
  by
  rw [← le_equalizer] at hS hT ⊢
  exact sup_le hS hT

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