exists_lt_card_finite_nth_eq — Mathlib

English

If hf is finite and p(x) holds, there exists n < #hf.toFinset with nth p n = x.

Русский

Если hf конечное и p(x) истинно, существует n < #hf.toFinset такое, что nth p n = x.

LaTeX

$$Theorem exists_lt_card_finite_nth_eq(hf)(h): ∃ n, n < #hf.toFinset ∧ nth p n = x.$$

Lean4

theorem exists_lt_card_finite_nth_eq (hf : (setOf p).Finite) {x} (h : p x) : ∃ n, n < #hf.toFinset ∧ nth p n = x := by
  rwa [← @Set.mem_setOf_eq _ _ p, ← image_nth_Iio_card hf] at h

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