image_val_iInter — Mathlib

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

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