hnot_inf_distrib — Mathlib

English

In a co-Heyting algebra, negation distributes over information (infimum) via a De Morgan-like law: ¬(a ∧ b) = ¬a ∨ ¬b.

Русский

В коэйтинговой алгебре отрицание над операцией ∧ распределяется по ∨ по де Моргану: ¬(a ∧ b) = ¬a ∨ ¬b.

LaTeX

$$$$ \neg (a \wedge b) = \neg a \vee \neg b $$$$

Lean4

theorem hnot_inf_distrib (a b : α) : ￢(a ⊓ b) = ￢a ⊔ ￢b := by simp_rw [← top_sdiff', sdiff_inf_distrib]

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