hnot_hnot_sup_distrib — Mathlib

English

Double negation distributes over join: ¬¬(a ∨ b) = ¬¬a ∨ ¬¬b.

Русский

Двойное отрицание распределяется над объединением: ¬¬(a ∨ b) = ¬¬a ∨ ¬¬b.

LaTeX

$$$\neg\neg(a \lor b) = \neg\neg a \lor \neg\neg b$$$

Lean4

theorem hnot_hnot_sup_distrib (a b : α) : ￢￢(a ⊔ b) = ￢￢a ⊔ ￢￢b :=
  by
  refine ((hnot_inf_distrib _ _).ge.trans <| hnot_anti le_hnot_inf_hnot).antisymm' ?_
  rw [hnot_le_iff_codisjoint_left, codisjoint_assoc, codisjoint_hnot_hnot_left_iff, codisjoint_left_comm,
    codisjoint_hnot_hnot_left_iff, ← codisjoint_assoc, sup_comm]
  exact codisjoint_hnot_right

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