forall_ge_iff

Mathlib.Order.BoundedOrder.Monotone

URI: https://scilib.ai/kg/mathlib#forall_ge_iff

English

Let P be monotone. Then (for all x with x ≥ x0, P x) is equivalent to P x0.

Русский

Пусть P монотонна. Тогда (для всех x ≥ x0, P x) эквивалентно P x0.

LaTeX

$$$\\\\forall x, x \\ge x_0 \\Rightarrow P x \\\\iff P x_0$$$

Lean4

theorem forall_ge_iff {P : α → Prop} {x₀ : α} (hP : Monotone P) : (∀ x ≥ x₀, P x) ↔ P x₀ :=
  ⟨fun H ↦ H x₀ le_rfl, fun H _ hx ↦ hP hx H⟩

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

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

Разделы

Аффилиация

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