English
If A is a Disjoint CantorScheme, then the second projection of the induced map is injective.
Русский
Если A — дизjoint CantorScheme, то вторая проекция индуцированного отображения инъективна.
LaTeX
$$$ CantorScheme.Disjoint A \Rightarrow Injective((CantorScheme.inducedMap A).snd). $$$
Lean4
/-- A scheme where the children of each set are pairwise disjoint induces an injective map. -/
theorem map_injective (hA : CantorScheme.Disjoint A) : Injective (inducedMap A).2 :=
by
rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
refine Subtype.coe_injective (res_injective ?_)
dsimp
ext n : 1
induction n with
| zero => simp
| succ n ih =>
simp only [res_succ, cons.injEq]
refine ⟨?_, ih⟩
contrapose hA
simp only [CantorScheme.Disjoint, _root_.Pairwise, Ne, not_forall, exists_prop]
refine ⟨res x n, _, _, hA, ?_⟩
rw [not_disjoint_iff]
refine ⟨(inducedMap A).2 ⟨x, hx⟩, ?_, ?_⟩
· rw [← res_succ]
apply map_mem
rw [hxy, ih, ← res_succ]
apply map_mem
