lowerClosure_smul — Mathlib

English

Let α be a commutative group with a compatible order. For any subset s ⊆ α and any a ∈ α, the downward closure of a·s equals a times the downward closure of s.

Русский

Пусть α — коммутативная группа с совместимым порядком. Для любого подмножества s ⊆ α и любого элемента a ∈ α выполняется, что нижнее замыкание множества a·s равно a·нижнему замыканию s.

LaTeX

$$$\forall a \in \alpha\,\forall s \subseteq \alpha:\; \operatorname{lowerClosure}(a \cdot s) = a \cdot \operatorname{lowerClosure}(s)$$$

Lean4

@[to_additive (attr := simp)]
theorem lowerClosure_smul : lowerClosure (a • s) = a • lowerClosure s :=
  lowerClosure_image <| OrderIso.mulLeft a

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