le_hnot_inf_hnot — Mathlib

English

In any co-Heyting algebra, the negation of a join is below the join of negations: ¬(a ∨ b) ≤ ¬a ∧ ¬b.

Русский

В любой коейтинговой алгебре отрицание объединения меньше или равно объединению отрицаний: ¬(a ∨ b) ≤ ¬a ∧ ¬b.

LaTeX

$$$\neg(a \lor b) \le \neg a \wedge \neg b$$$

Lean4

theorem le_hnot_inf_hnot : ￢(a ⊔ b) ≤ ￢a ⊓ ￢b :=
  le_inf (hnot_anti le_sup_left) <| hnot_anti le_sup_right

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