lawsonOpen_iff_scottOpen_of_isUpperSet'

English

An upper set is Lawson open if and only if it is Scott open, in a setting with isLawson and isScott assumptions.

Русский

В условии IsLawson и IsScott верхнее множество открыто в Lawson тогда и только тогда когда оно открыто в Scott.

LaTeX

$$$IsOpen_{lawson}(s) \iff IsOpen_{scott}(s)$ under IsUpperSet s and lawson/scott assumptions$$

Lean4

/-- An upper set is Lawson open if and only if it is Scott open -/
theorem lawsonOpen_iff_scottOpen_of_isUpperSet' (s : Set α) (h : IsUpperSet s) : IsOpen[L] s ↔ IsOpen[S] s :=
  by
  rw [@IsLawson.topology_eq_lawson α _ L _, @IsScott.topology_eq α univ _ S _]
  exact lawsonOpen_iff_scottOpen_of_isUpperSet h

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