isGreatest_himp — Mathlib

English

In a generalized Heyting algebra, for any a,b, the element a ⇨ b is the greatest w such that w ⊓ a ≤ b.

Русский

В обобщенной аддитивной логике Хейтинга элемент a ⇨ b есть наибольшее w такой, что w ∧ a ≤ b.

LaTeX

$$IsGreatest {w | w ⊓ a ≤ b} (a ⇨ b)$$

Lean4

theorem isGreatest_himp [GeneralizedHeytingAlgebra α] (a b : α) : IsGreatest {w | w ⊓ a ≤ b} (a ⇨ b) := by
  simp [IsGreatest, mem_upperBounds]

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