image₂_inter_right — Mathlib

English

If f is injective2, then image₂ f s (t ∩ t') = image₂ f s t ∩ image₂ f s t'.

Русский

Если f инъективна в двух аргументах, то образ_2 сохраняет пересечение по правой стороне: image₂ f s (t ∩ t') = image₂ f s t ∩ image₂ f s t'.

LaTeX

$$$\\operatorname{image}_2 f s (t \\cap t') = \\operatorname{image}_2 f s t \\cap \\operatorname{image}_2 f s t'$$$

Lean4

theorem image₂_inter_right [DecidableEq β] (hf : Injective2 f) : image₂ f s (t ∩ t') = image₂ f s t ∩ image₂ f s t' :=
  coe_injective <| by
    push_cast
    exact image2_inter_right hf

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