isLowerSet_preimage_ofDual_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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