sup_inf_distrib_left — Mathlib

English

Distributivity of meet over join on CauSeq: (a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c).

Русский

Существует дисптрибутивность: (a ∧ b) ∨ c = (a ∨ c) ∧ (b ∨ c).

LaTeX

$$$a,b,c \in \mathrm{CauSeq}(\alpha, \mathrm{abs}) \Rightarrow (a \wedge b) \vee c = (a \vee c) \wedge (b \vee c)$$$

Lean4

protected theorem sup_inf_distrib_left (a b c : CauSeq α abs) : a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c) :=
  ext fun _ ↦ max_min_distrib_left _ _ _

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