inf_le_inf

Mathlib.Order.Lattice

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

English

If a ≤ b and c ≤ d, then a ⊓ c ≤ b ⊓ d.

Русский

Если a ≤ b и c ≤ d, то a ⊓ c ≤ b ⊓ d.

LaTeX

$$$ a \le b \quad \land \quad c \le d \Rightarrow a \sqcap c \le b \sqcap d $$$

Lean4

@[gcongr]
theorem inf_le_inf (h₁ : a ≤ b) (h₂ : c ≤ d) : a ⊓ c ≤ b ⊓ d :=
  @sup_le_sup αᵒᵈ _ _ _ _ _ h₁ h₂

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

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

Разделы

Аффилиация

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