lawsonClosed_iff_scottClosed_of_isLowerSet

English

For any L, S with IsLawson and IsScott, a set is Lawson closed iff it is Scott closed when it is a lower set.

Русский

Для множества s, являющегося нижним набором IsLowerSet, замкнутость в Lawson эквивалентна замкнутости в Scott.

LaTeX

$$$(s: Set α), IsLowerSet s \rightarrow (IsClosed_{lawson}(s) \leftrightarrow IsClosed_{scott}(s))$$$

Lean4

theorem lawsonClosed_iff_scottClosed_of_isLowerSet (s : Set α) (h : IsLowerSet s) : IsClosed[L] s ↔ IsClosed[S] s := by
  rw [← @isOpen_compl_iff, ← isOpen_compl_iff, (lawsonOpen_iff_scottOpen_of_isUpperSet' L S _ (isUpperSet_compl.mpr h))]

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