instHeytingAlgebra — Mathlib

English

The nuclei are equipped with a Heyting algebra structure; they form a rich logic of implications and negations.

Русский

Нуклеусы образуют структуру Heyting-алгебры, давая логику импликаций и отрицаний.

LaTeX

$$$\text{HeytingAlgebra}(Nucleus(X))$$$

Lean4

instance : HeytingAlgebra (Nucleus X) where
  compl m := m ⇨ ⊥
  le_himp_iff _ n
    _ := by simpa [← coe_le_coe, Pi.le_def] using ⟨fun h i ↦ h i i le_rfl, fun h i j _ ↦ (h j).trans' <| by gcongr⟩
  himp_bot m := rfl

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