isUpperSet_preimage_toDual_iff — Mathlib

English

Let α be a partially ordered set. For any subset s of the dual order α^op, s is an upper set in α^op if and only if s is a lower set in α.

Русский

Пусть α — частично упорядоченное множество. Пусть s ⊆ α^op; тогда s является верхним множеством в α^op тогда и только тогда, когда оно является нижним множеством в α.

LaTeX

$$$IsUpperSet\\bigl(\\operatorname{toDual}^{-1}(s)\\bigr) \\iff IsLowerSet(s)$$$

Lean4

@[simp]
theorem isUpperSet_preimage_toDual_iff {s : Set αᵒᵈ} : IsUpperSet (toDual ⁻¹' s) ↔ IsLowerSet s :=
  Iff.rfl

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