dependent_image — Mathlib

English

The image of a finite dependent family over a finite index set is finite.

Русский

Образ конечной зависимой семьи по конечному индексу конечен.

LaTeX

$$$ \text{Finite}\left(\{ y \in \beta \mid \exists x \in s, F(x,x\!\_2)=y \} \right)$ where $s$ is finite.$$

Lean4

theorem dependent_image {s : Set α} (hs : s.Finite) (F : ∀ i ∈ s, β) : {y : β | ∃ x hx, F x hx = y}.Finite :=
  by
  have := hs.to_subtype
  simpa [range] using finite_range fun x : s => F x x.2

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