image_nth_Iio_card — Mathlib

English

For finite hf, the image of nth p on Set.Iio (#hf.toFinset) equals setOf p.

Русский

Для конечного hf образ nth p на Set.Iio (#hf.toFinset) равен setOf p.

LaTeX

$$For hf finite, nth p '' Set.Iio #hf.toFinset = setOf p.$$

Lean4

@[simp]
theorem image_nth_Iio_card (hf : (setOf p).Finite) : nth p '' Set.Iio #hf.toFinset = setOf p :=
  calc
    nth p '' Set.Iio #hf.toFinset = Set.range (hf.toFinset.orderEmbOfFin rfl) :=
      by
      ext x
      simp only [Set.mem_image, Set.mem_range, Fin.exists_iff, ← nth_eq_orderEmbOfFin hf, Set.mem_Iio, exists_prop]
    _ = setOf p := by rw [range_orderEmbOfFin, Set.Finite.coe_toFinset]

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