nth_mem_of_lt_card

Mathlib.Data.Nat.Nth

URI: https://scilib.ai/kg/mathlib#Nat.nth_mem_of_lt_card

← MathLib Explorer

English

If hf is finite and hlt: n < #hf.toFinset, then p (nth p n).

Русский

Если hf конечное и n < #hf.toFinset, то p(nth p n).

LaTeX

$$nth p n ∈ setOf p$$

Lean4

theorem nth_mem_of_lt_card {n : ℕ} (hf : (setOf p).Finite) (hlt : n < #hf.toFinset) : p (nth p n) :=
  (image_nth_Iio_card hf).subset <| Set.mem_image_of_mem _ hlt

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru