coe_sup — Mathlib

English

The carrier of max s t equals the closure of the carrier of s.toSubmodule ⊔ t.toSubmodule.

Русский

Carrier максимума s и t равен замыканию carrier(s.toSubmodule ⊔ t.toSubmodule).

LaTeX

$$$\uparrow(\operatorname{ClosedSubmodule.max}(s,t)) = closure (s.toSubmodule \sqcup t.toSubmodule).carrier$$$

Lean4

@[simp, norm_cast]
theorem coe_sup : ↑(s ⊔ t) = closure (s.toSubmodule ⊔ t.toSubmodule).carrier :=
  by
  simp only [← coe_toSubmodule, toSubmodule_sup]
  simp only [coe_toSubmodule, Submodule.coe_closure, Submodule.carrier_eq_coe]

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