English
The image of the intersection over i of t_i equals the intersection over i of the images.
Русский
Образ пересечения по i множества t_i равен пересечению образов.
LaTeX
$$$\\operatorname{image}(\\operatorname{val})(\\bigcap_i t_i) = \\bigcap_i (\\operatorname{image}(\\operatorname{val})(t_i))$$$
Lean4
@[simp]
theorem image_val_iInter [Nonempty ι] : (↑(⋂ i, t i) : Set α) = ⋂ i, (↑(t i) : Set α) :=
Subtype.val_injective.injOn.image_iInter_eq