mem_rangeFin — Mathlib

English

Membership in the range of a Fin-range construction is equivalent to existence of an index mapping to the element.

Русский

Членство в диапазоне диапазона Fin эквивалентно существованию индекса, для которого f(k) равно данному элементу.

LaTeX

$$$x \in \mathrm{rangeFin}(f,h_0,h_{ ext{last}},h_{covBy}) \iff \exists k, f(k) = x.$$$

Lean4

@[simp]
theorem mem_rangeFin {x h0 hlast hcovBy} : x ∈ rangeFin f h0 hlast hcovBy ↔ ∃ k, f k = x :=
  Iff.rfl

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