lawsonClosed_iff_dirSupClosed_of_isLowerSet

English

A lower set is Lawson closed iff it is closed under directed suprema.

Русский

Нижнее множество замкнуто в Lawson тогда и только тогда, когда оно замкнуто по направленным наивысшим пределам.

LaTeX

$$$\forall (L S) [IsLawson α] [IsScott α Set.univ], (s: Set α), IsLowerSet s \rightarrow (IsClosed(s) \leftrightarrow DirSupClosed s)$$$

Lean4

/-- A lower set is Lawson closed if and only if it is closed under sups of directed sets -/
theorem lawsonClosed_iff_dirSupClosed_of_isLowerSet (s : Set α) (h : IsLowerSet s) : IsClosed[L] s ↔ DirSupClosed s :=
  by
  rw [lawsonClosed_iff_scottClosed_of_isLowerSet L S _ h, @IsScott.isClosed_iff_isLowerSet_and_dirSupClosed]
  simp_all

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