himp_eq_sSup — Mathlib

English

In a frame α, the Heyting implication a ⇒ b equals the supremum of all w such that w ∧ a ≤ b.

Русский

В рамке α импликация Хейтинга a ⇒ b равна наибольшему верхнему пределу всех w, удовлетворяющих w ∧ a ≤ b.

LaTeX

$$$a \Rightarrow b = \operatorname{sSup} \{ w \mid w \wedge a \le b \}$$$

Lean4

theorem himp_eq_sSup : a ⇨ b = sSup {w | w ⊓ a ≤ b} :=
  (isGreatest_himp a b).isLUB.sSup_eq.symm

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