codisjoint_hnot_hnot_right_iff — Mathlib

English

Let a, b be elements of a co-Heyting algebra. Then Codisjoint a (¬¬b) is equivalent to Codisjoint a b.

Русский

Пусть a, b — элементы коейтинговой алгебры. Тогда Codisjoint a (¬¬b) эквивалентно Codisjoint a b.

LaTeX

$$$\mathrm{Codisjoint}(a, \neg\neg b) \iff \mathrm{Codisjoint}(a,b)$$$

Lean4

@[simp]
theorem codisjoint_hnot_hnot_right_iff : Codisjoint a (￢￢b) ↔ Codisjoint a b := by
  simp_rw [← hnot_le_iff_codisjoint_left, hnot_hnot_hnot]

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