upperClosure_smul — Mathlib

English

The upper closure commutes with smul: upperClosure (a • S) = a • upperClosure S for any a ∈ α and S ⊆ α.

Русский

Верхняя замкнутость коммутирует с умножением на скаляр: upperClosure (a • S) = a • upperClosure S.

LaTeX

$$$\\text{upperClosure}(a \\cdot S) = a \\cdot \\text{upperClosure}(S)$$$

Lean4

@[to_additive (attr := simp)]
theorem upperClosure_smul : upperClosure (a • s) = a • upperClosure s :=
  upperClosure_image <| OrderIso.mulLeft a

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