isUpperSet_compl — Mathlib

English

An upper set is exactly the complement of a lower set, and conversely: IsUpperSet(s^c) ↔ IsLowerSet(s).

Русский

Верхнее множество является дополнением к нижнему множеству и наоборот: IsUpperSet(s^c) ⇔ IsLowerSet(s).

LaTeX

$$$IsUpperSet s^c \leftrightarrow IsLowerSet s$$$

Lean4

@[simp]
theorem isUpperSet_compl : IsUpperSet sᶜ ↔ IsLowerSet s :=
  ⟨fun h => by
    convert h.compl
    rw [compl_compl], IsLowerSet.compl⟩

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