isLowerSet_compl — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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