subset_pi_eval_image — Mathlib

English

For a fixed set s ⊆ ι, the set u is contained in the product of eval images over s.

Русский

Для фиксированного множества s ⊆ ι множество u содержится в произведении изображений eval по i ∈ s.

LaTeX

$$$$ u \\subseteq \\pi s (\\lambda i. \\operatorname{eval}_i'' u). $$$$

Lean4

theorem subset_pi_eval_image (s : Set ι) (u : Set (∀ i, α i)) : u ⊆ pi s fun i => eval i '' u := fun f hf _ _ =>
  ⟨f, hf, rfl⟩

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