English
For a nonempty family T, the image of the intersection equals the intersection of the images.
Русский
Для непустого семейства T образ пересечения равен пересечению образов.
LaTeX
$$$\\operatorname{image}(\\operatorname{val})(\\bigcap_0 T) = \\bigcap_0 \\{ \\operatorname{image}(\\operatorname{val}) B \\mid B \\in T \\}$, with T.Nonempty$$
Lean4
@[simp]
theorem image_val_sInter (hT : T.Nonempty) : (↑(⋂₀ T) : Set α) = ⋂₀ {(↑B : Set α) | B ∈ T} := by
rw [← Set.image, sInter_image, sInter_eq_biInter, Subtype.val_injective.injOn.image_biInter_eq hT]