hnot_hnot_sdiff_distrib — Mathlib

English

Double negation distributes over relative difference: ¬¬(a \ b) = ¬¬a \ ¬¬b.

Русский

Двойное отрицание распределяется над относительной разностью: ¬¬(a \ b) = ¬¬a \ ¬¬b.

LaTeX

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

Lean4

theorem hnot_hnot_sdiff_distrib (a b : α) : ￢￢(a \ b) = ￢￢a \ ￢￢b :=
  by
  apply le_antisymm
  · refine hnot_le_comm.1 ((hnot_anti sdiff_le_inf_hnot).trans' ?_)
    rw [hnot_inf_distrib, hnot_le_iff_codisjoint_right, codisjoint_left_comm, ← hnot_le_iff_codisjoint_right]
    exact le_sdiff_sup
  · rw [sdiff_le_iff, ← hnot_hnot_sup_distrib]
    exact hnot_anti (hnot_anti le_sup_sdiff)

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