boundary_sup_sup_boundary_inf — Mathlib

English

Equality: ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b) = ∂ a ⊔ ∂ b.

Русский

Равенство: ∂(a ∨ b) ∨ ∂(a ∧ b) = ∂a ∨ ∂b.

LaTeX

$$$ ∂ (a \vee b) \;\square\; ∂ (a \wedge b) = ∂ a \vee ∂ b $$$

Lean4

theorem boundary_sup_sup_boundary_inf (a b : α) : ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b) = ∂ a ⊔ ∂ b :=
  le_antisymm (sup_le boundary_sup_le boundary_inf_le) <|
    sup_le boundary_le_boundary_sup_sup_boundary_inf_left boundary_le_boundary_sup_sup_boundary_inf_right

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