boundary_le_boundary_sup_sup_boundary_inf_left

English

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

Русский

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

LaTeX

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

Lean4

theorem boundary_le_boundary_sup_sup_boundary_inf_left : ∂ a ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b) :=
  by
  simp only [boundary, sup_inf_left, sup_inf_right, sup_right_idem, le_inf_iff, sup_assoc, sup_comm _ a]
  refine ⟨⟨⟨?_, ?_⟩, ⟨?_, ?_⟩⟩, ?_, ?_⟩ <;>
      try { exact le_sup_of_le_left inf_le_left
      } <;>
    refine inf_le_of_right_le ?_
  · rw [hnot_le_iff_codisjoint_right, codisjoint_left_comm]
    exact codisjoint_hnot_left
  · refine le_sup_of_le_right ?_
    rw [hnot_le_iff_codisjoint_right]
    exact codisjoint_hnot_right.mono_right (hnot_anti inf_le_left)

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