covBy_iff_lt_iff_le_left

Mathlib.Order.Cover

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

← MathLib Explorer

English

If a ⋖ b, then Icc(a,b) = {a, b}.

Русский

Если a ⋖ b, то Icc(a,b) = {a, b}.

LaTeX

$$Icc(a,b) = \{ a, b \}$$

Lean4

theorem covBy_iff_lt_iff_le_left {x y : α} : x ⋖ y ↔ ∀ {z}, z < y ↔ z ≤ x
    where
  mp := fun hx _z ↦ ⟨hx.le_of_lt, fun hz ↦ hz.trans_lt hx.lt⟩
  mpr := fun H ↦ ⟨H.2 le_rfl, fun _z hx hz ↦ (H.1 hz).not_gt hx⟩

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

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

Разделы

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

Аффилиация

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