English
The smul of a submonoid with a supremum equals the supremum of the smuls: M • (N ⊔ P) = M • N ⊔ M • P.
Русский
Скалярное умножение подмножества на верхнюю границу равно верхней границе скалярного умножения по каждому из слагаемых: M • (N ⊔ P) = M • N ⊔ M • P.
LaTeX
$$$M \cdot (N \sqcup P) = M \cdot N \sqcup M \cdot P$$$
Lean4
theorem addSubmonoid_smul_sup : M • (N ⊔ P) = M • N ⊔ M • P :=
le_antisymm
(smul_le.mpr fun m hm np hnp ↦
by
refine closure_induction (motive := (fun _ ↦ _ • · ∈ _)) ?_ ?_ ?_ (sup_eq_closure N P ▸ hnp)
· rintro x (hx | hx)
exacts [le_sup_left (a := M • N) (smul_mem_smul hm hx), le_sup_right (a := M • N) (smul_mem_smul hm hx)]
· apply (smul_zero (A := A) m).symm ▸ (M • N ⊔ M • P).zero_mem
· intro _ _ _ _ h1 h2; rw [smul_add]; exact add_mem h1 h2)
(sup_le (smul_le_smul_right le_sup_left) <| smul_le_smul_right le_sup_right)
