English
The intersection of the ranges of ι_i and ι_j equals the range of the composed map D.f i j ≫ ι_.
Русский
Пересечение диапазонов ι_i и ι_j равно диапазону композиции D.f i j ≫ ι_.
LaTeX
$$$\mathrm{range}(\iota_i) \cap \mathrm{range}(\iota_j) = \mathrm{range}(D.f i j \; \gg\; \iota _)$$$
Lean4
theorem image_inter (i j : D.J) : Set.range (𝖣.ι i) ∩ Set.range (𝖣.ι j) = Set.range (D.f i j ≫ 𝖣.ι _) :=
by
ext x
constructor
· rintro ⟨⟨x₁, eq₁⟩, ⟨x₂, eq₂⟩⟩
obtain ⟨y, e₁, -⟩ := (D.ι_eq_iff_rel _ _ _ _).mp (eq₁.trans eq₂.symm)
· substs eq₁
exact ⟨y, by simp [e₁]⟩
· rintro ⟨x, hx⟩
refine ⟨⟨D.f i j x, hx⟩, ⟨D.f j i (D.t _ _ x), ?_⟩⟩
rw [D.glue_condition_apply]
exact hx
