pow_right_monotone

Mathlib.Algebra.Group.Pointwise.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.pow_right_monotone

English

If 1 ∈ s, then the map n ↦ s^n is monotone with respect to inclusion on natural numbers.

Русский

Если 1 ∈ s, то отображение n ↦ s^n монотонно по включению на естественных числах.

LaTeX

$$$$ (hs : 1 \in s) \Rightarrow \mathrm{Monotone}(n \mapsto s^n). $$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru