range_orderEmbOfFin — Mathlib

English

Let s be a finite subset of α with card k. Then the range of the order embedding s.orderEmbOfFin h is exactly s.

Русский

Пусть s — конечное множество α с кардиналом k. Тогда образ отображения s.orderEmbOfFin h равен s.

LaTeX

$$Set.range (s.orderEmbOfFin h) = s$$

Lean4

@[simp]
theorem range_orderEmbOfFin (s : Finset α) {k : ℕ} (h : s.card = k) : Set.range (s.orderEmbOfFin h) = s := by
  simp only [orderEmbOfFin, Set.range_comp ((↑) : _ → α) (s.orderIsoOfFin h), RelEmbedding.coe_trans, Set.image_univ,
    Finset.orderEmbOfFin, RelIso.range_eq, OrderEmbedding.coe_subtype, OrderIso.coe_toOrderEmbedding,
    Subtype.range_coe_subtype, Finset.setOf_mem]

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