sup_le_iff

Mathlib.Order.Lattice

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

← MathLib Explorer

English

a ⊔ b ≤ c if and only if a ≤ c and b ≤ c.

Русский

a ⊔ b ≤ c тогда и только тогда, когда a ≤ c и b ≤ c.

LaTeX

$$$a \\oplus b \\le c \\iff (a \\le c) \\land (b \\le c)$$$

Lean4

@[simp]
theorem sup_le_iff : a ⊔ b ≤ c ↔ a ≤ c ∧ b ≤ c :=
  ⟨fun h : a ⊔ b ≤ c => ⟨le_trans le_sup_left h, le_trans le_sup_right h⟩, fun ⟨h₁, h₂⟩ => sup_le h₁ h₂⟩

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

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

Разделы

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

Аффилиация

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