mem_mk — Mathlib

English

Let α be a set with a partial order and s a subset of α that is upward closed. The canonical upper set built from s has the same underlying elements as s; i.e., an element a belongs to the constructed UpperSet if and only if a belongs to s.

Русский

Пусть α упорядочено; пусть s ⊆ α является верхним открытым множеством. Каноническое верхнее множество, построенное из s, содержит ровно те элементы, что принадлежат s; то есть a ∈ UpperSet(s) тогда и только тогда, когда a ∈ s.

LaTeX

$$$a \in \mathrm{mk}(s, hs) \iff a \in s$$$

Lean4

@[simp]
theorem mem_mk {s : Set α} (hs) {a : α} : a ∈ mk s hs ↔ a ∈ s :=
  Iff.rfl

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