top_mem_insertTop — Mathlib

English

There exists an order-embedding that lifts finite subsets of α to finite subsets of WithTop α by inserting a top element.

Русский

Существует отображение по порядку, переводя конечные подмножества α в конечные подмножества WithTop α путём добавления верхнего элемента.

LaTeX

$$$ insertTop : Finset\,\alpha \hookrightarrow_o Finset\,(WithTop\,\alpha) \\;\; \text{defined by } s \mapsto \{\top\} \cup (s \mapsto \operatorname{coeWithTop}(s)) $$$

Lean4

@[simp]
theorem top_mem_insertTop {s : Finset α} : ⊤ ∈ insertTop s := by simp [insertTop]

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