boundary_sup_le — Mathlib

English

For all a,b, ∂(a ⊔ b) ≤ ∂ a ⊔ ∂ b.

Русский

Для любых a,b: ∂(a ∨ b) ≤ ∂ a ∨ ∂ b.

LaTeX

$$$ ∂ (a \vee b) \le ∂ a \vee ∂ b $$$

Lean4

theorem boundary_sup_le : ∂ (a ⊔ b) ≤ ∂ a ⊔ ∂ b :=
  by
  rw [boundary, inf_sup_right]
  exact
    sup_le_sup (inf_le_inf_left _ <| hnot_anti le_sup_left)
      (inf_le_inf_left _ <| hnot_anti le_sup_right)
        /- The intuitionistic version of `Coheyting.boundary_le_boundary_sup_sup_boundary_inf_left`. Either
        proof can be obtained from the other using the equivalence of Heyting algebras and intuitionistic
        logic and duality between Heyting and co-Heyting algebras. It is crucial that the following proof be
        intuitionistic. -/

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