infPrime_toDual — Mathlib

English

In a semilattice with join, taking InfPrime on the dual of an element is equivalent to taking SupPrime on the element itself.

Русский

В полуполе с операцией объединения InfPrime над двойственным порядком элемента эквивалентен SupPrime над самим элементом.

LaTeX

$$$\InfPrime(a^{\ast}) \iff \SupPrime(a)$$$

Lean4

@[simp]
theorem infPrime_toDual {a : α} : InfPrime (toDual a) ↔ SupPrime a :=
  Iff.rfl

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