supClosed_preimage_toDual — Mathlib

English

In the dual order, SupClosed of the preimage under toDual is equivalent to InfClosed of the original set.

Русский

В двойственном порядке замыкание по верхним границам образуется через инф-замыкание исходного множества.

LaTeX

$$SupClosed( toDual^{-1}' s ) ↔ InfClosed s$$

Lean4

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

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