covBy_iff_le_iff_lt_left

Mathlib.Order.Cover

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

English

If a ⋖ b, then Ioi(a) = Ici(b).

Русский

Если a ⋖ b, то Ioi(a) = Ici(b).

LaTeX

$$Ioi(a) = ICI(b)$$

Lean4

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

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

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

Разделы

Аффилиация

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