covBy_iff_lt_iff_le_right

Mathlib.Order.Cover

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

← MathLib Explorer

English

If a ⋖ b, then Iio(b) = Iic(a).

Русский

Если a ⋖ b, то Iio(b) = Iic(a).

LaTeX

$$Iio(b) = Iic(a)$$

Lean4

theorem covBy_iff_lt_iff_le_right {x y : α} : x ⋖ y ↔ ∀ {z}, x < z ↔ y ≤ z :=
  by
  trans ∀ {z}, ¬z ≤ x ↔ ¬z < y
  · simp_rw [covBy_iff_le_iff_lt_left, not_iff_not]
  · simp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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