inf_left_le_of_le_sup_right — Mathlib

English

If x and y are complements and a ≤ b ∨ y, then a ∧ x ≤ b.

Русский

Если x и y комплементы и a ≤ b ∨ y, то a ∧ x ≤ b.

LaTeX

$$$$ IsCompl(x,y) \rightarrow (a \le b \vee y) \rightarrow (a \wedge x \le b). $$$$

Lean4

theorem inf_left_le_of_le_sup_right (h : IsCompl x y) (hle : a ≤ b ⊔ y) : a ⊓ x ≤ b :=
  calc
    a ⊓ x ≤ (b ⊔ y) ⊓ x := inf_le_inf hle le_rfl
    _ = b ⊓ x ⊔ y ⊓ x := (inf_sup_right _ _ _)
    _ = b ⊓ x := by rw [h.symm.inf_eq_bot, sup_bot_eq]
    _ ≤ b := inf_le_left

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