inf_le_iff

Mathlib.Order.Lattice

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

English

In a linear order α, the infimum of b and c is below a if and only if either b ≤ a or c ≤ a.

Русский

В линейном порядке α наименьшее из b и c не выше a тогда и только тогда, когда либо b ≤ a, либо c ≤ a.

LaTeX

$$$ b \sqcap c \le a \iff b \le a \lor c \le a $$$

Lean4

@[simp]
theorem inf_le_iff : b ⊓ c ≤ a ↔ b ≤ a ∨ c ≤ a :=
  @le_sup_iff αᵒᵈ _ _ _ _

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

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

Разделы

Аффилиация

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