map_hnot — Mathlib

English

Let f be a homomorphism between co-Heyting algebras. Then f preserves negation: for every a, f(¬a) = ¬f(a).

Русский

Пусть f — гомоморфизм когейтинговых алгебр. Тогда f сохраняет отрицание: для любого a выполняется f(¬a) = ¬f(a).

LaTeX

$$$f(\\neg a) = \\neg f(a)$$$

Lean4

@[simp]
theorem map_hnot (a : α) : f (￢a) = ￢f a := by rw [← top_sdiff', ← top_sdiff', map_sdiff, map_top]

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