isUpperSet_preimage_ofDual_iff — Mathlib

English

IsUpperSet of the preimage under the dual is equivalent to IsLowerSet of the original set: IsUpperSet(ofDual^{-1}(s)) ↔ IsLowerSet(s).

Русский

Верхнее множество через прообраз двойного порядка эквивалентно нижнему множеству исходного: IsUpperSet(ofDual^{-1}(s)) ⇔ IsLowerSet(s).

LaTeX

$$$IsUpperSet(\mathrm{ofDual}^{-1}(s)) \iff IsLowerSet(s)$$$

Lean4

@[simp]
theorem isUpperSet_preimage_ofDual_iff : IsUpperSet (ofDual ⁻¹' s) ↔ IsLowerSet s :=
  Iff.rfl

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