subset_eval_image_pi — Mathlib

English

For any s and t, and any i, t i is contained in the image of s.pi t under eval i.

Русский

Для любых s, t и i, t_i ⊆ образ eval_i от s.pi t.

LaTeX

$$$ \forall i,\ t_i \subseteq \mathrm{image}(\mathrm{eval}_i)(s.\pi t) $$$

Lean4

theorem subset_eval_image_pi (ht : (s.pi t).Nonempty) (i : ι) : t i ⊆ eval i '' s.pi t := by
  classical
  obtain ⟨f, hf⟩ := ht
  refine fun y hy => ⟨update f i y, fun j hj => ?_, update_self ..⟩
  obtain rfl | hji := eq_or_ne j i <;> simp [*, hf _ hj]

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