isLowerSet_of_isClosed — Mathlib

English

Let α be a preorder with a topology and IsUpper. If a subset s ⊆ α is closed, then s is downward closed; that is, if x ∈ s and y ≤ x, then y ∈ s.

Русский

Пусть α — частично упорядоченное множество с топологией и свойством IsUpper. Если подмножество s ⊆ α замкнуто, то оно является нижним множеством: если x ∈ s и y ≤ x, то y ∈ s.

LaTeX

$$$\text{IsClosed}(s) \rightarrow \text{IsLowerSet}(s)$$$

Lean4

theorem isLowerSet_of_isClosed (h : IsClosed s) : IsLowerSet s :=
  isUpperSet_compl.1 <| isUpperSet_of_isOpen h.isOpen_compl

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