instPow

Mathlib.Algebra.Order.Interval.Set.Instances

URI: https://scilib.ai/kg/mathlib#Set.Ioc.instPow

English

Powers of elements of Ioc(0,1) stay in Ioc(0,1).

Русский

Степени элементов Ioc(0,1) остаются в Ioc(0,1).

LaTeX

$$$\forall x \in (0,1],\ \forall n \in \mathbb{N},\ 0 < x^n \le 1$$$

Lean4

instance instPow : Pow (Ioc (0 : R) 1) ℕ where
  pow p n := ⟨p.1 ^ n, ⟨pow_pos p.2.1 n, pow_le_one₀ (le_of_lt p.2.1) p.2.2⟩⟩

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

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

Разделы

Аффилиация

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