isGreatest_compl — Mathlib

English

In a Heyting algebra, the complement aᶜ is the greatest w such that Disjoint w a.

Русский

В гейтинговой алгебре дополнение aᶜ есть наибольшее w, удовлетворяющее условию Disjoint w a.

LaTeX

$$IsGreatest {w | Disjoint w a} (aᶜ)$$

Lean4

theorem isGreatest_compl [HeytingAlgebra α] (a : α) : IsGreatest {w | Disjoint w a} (aᶜ) := by
  simpa only [himp_bot, disjoint_iff_inf_le] using isGreatest_himp a ⊥

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