eval_image_pi — Mathlib

English

If i ∈ s and (s.pi t) is nonempty, then the image of s.pi t under eval i equals t i.

Русский

Если i ∈ s и (s.pi t) непусто, то образ eval_i от s.pi t равен t_i.

LaTeX

$$$ \text{If } i \in s \text{ and } (s.\pi t) \neq \emptyset, \ \mathrm{image}(\mathrm{eval}_i)(s.\pi t) = t_i$$$

Lean4

theorem eval_image_pi (hs : i ∈ s) (ht : (s.pi t).Nonempty) : eval i '' s.pi t = t i :=
  (eval_image_pi_subset hs).antisymm (subset_eval_image_pi ht i)

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