forall_le_iff

Mathlib.Order.BoundedOrder.Monotone

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

English

Let P be Antitone. 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 \\le x_0 \\Rightarrow P x \\\\iff P x_0$$$

Lean4

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

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

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

Разделы

Аффилиация

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