le_of_inf_le_sup_le — Mathlib

English

If x ∧ z ≤ y ∧ z and x ∨ z ≤ y ∨ z, then x ≤ y.

Русский

Если x ∧ z ≤ y ∧ z и x ∨ z ≤ y ∨ z, то x ≤ y.

LaTeX

$$$\big( x \wedge z \le y \wedge z \big) \rightarrow \big( x \vee z \le y \vee z \big) \rightarrow x \le y$$$

Lean4

theorem le_of_inf_le_sup_le (h₁ : x ⊓ z ≤ y ⊓ z) (h₂ : x ⊔ z ≤ y ⊔ z) : x ≤ y :=
  calc
    x ≤ y ⊓ z ⊔ x := le_sup_right
    _ = (y ⊔ x) ⊓ (x ⊔ z) := by rw [sup_inf_right, sup_comm x]
    _ ≤ (y ⊔ x) ⊓ (y ⊔ z) := (inf_le_inf_left _ h₂)
    _ = y ⊔ x ⊓ z := by rw [← sup_inf_left]
    _ ≤ y ⊔ y ⊓ z := (sup_le_sup_left h₁ _)
    _ ≤ _ := sup_le (le_refl y) inf_le_left

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