covBy_iff_le_iff_lt_right

Mathlib.Order.Cover

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

English

covBy x y is equivalent to the statement that for all z, z < y iff z ≤ x.

Русский

covBy x y эквивалентно тому, что для всех z, z < y эквивалентно z ≤ x.

LaTeX

$${x y : α} : x \arbitrary CovBy y ↔ ∀ {z}, z < y ↔ z ≤ x$$

Lean4

theorem covBy_iff_le_iff_lt_right {x y : α} : x ⋖ y ↔ ∀ {z}, y ≤ z ↔ x < z := by
  simp_rw [covBy_iff_lt_iff_le_right, iff_comm]

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

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

Разделы

Аффилиация

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