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]