inf_sup_left — Mathlib

English

In a distributive lattice, a ∧ (b ∨ c) equals a ∧ b ∨ a ∧ c.

Русский

В распределительной решётке a ∧ (b ∨ c) = a ∧ b ∨ a ∧ c.

LaTeX

$$$ a \wedge (b \vee c) = a \wedge b \vee a \wedge c$$$

Lean4

theorem inf_sup_left (a b c : α) : a ⊓ (b ⊔ c) = a ⊓ b ⊔ a ⊓ c :=
  calc
    a ⊓ (b ⊔ c) = a ⊓ (a ⊔ c) ⊓ (b ⊔ c) := by rw [inf_sup_self]
    _ = a ⊓ (a ⊓ b ⊔ c) := by simp only [inf_assoc, sup_inf_right]
    _ = (a ⊔ a ⊓ b) ⊓ (a ⊓ b ⊔ c) := by rw [sup_inf_self]
    _ = (a ⊓ b ⊔ a) ⊓ (a ⊓ b ⊔ c) := by rw [sup_comm]
    _ = a ⊓ b ⊔ a ⊓ c := by rw [sup_inf_left]

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