forall_finite_image_eval_iff — Mathlib

English

Let δ be finite and κ: δ → Type, s ⊆ ∏_{d∈δ} κ(d). Then s is finite iff for every d, the projection eval d '' s is finite.

Русский

Пусть δ конечно, κ: δ → Type, s ⊆ ∏_{d∈δ} κ(d). Тогда множество s конечно тогда и только тогда, когда для каждого d проекция eval_d(s) конечна.

LaTeX

$$$(\\forall d:\\delta, (\\operatorname{Finite}(\\operatorname{eval}_d'' s))) \\iff \\operatorname{Finite}(s).$$$

Lean4

theorem forall_finite_image_eval_iff {δ : Type*} [Finite δ] {κ : δ → Type*} {s : Set (∀ d, κ d)} :
    (∀ d, (eval d '' s).Finite) ↔ s.Finite :=
  ⟨fun h => (Finite.pi h).subset <| subset_pi_eval_image _ _, fun h _ => h.image _⟩

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