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)