pow_right_monotone — Mathlib

English

If 1 is in s, then the map n ↦ s^n is monotone with respect to inclusion: m ≤ n implies s^m ⊆ s^n.

Русский

Если 1 ∈ s, то отображение n ↦ s^n монотонно относительно включения: при m ≤ n имеем s^m ⊆ s^n.

LaTeX

$$$1 \in s \\implies (m \\le n \\Rightarrow s^m \\subseteq s^n)$$$

Lean4

@[to_additive]
protected theorem pow_right_monotone (hs : 1 ∈ s) : Monotone (s ^ ·) :=
  pow_right_monotone <| one_subset.2 hs

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