English
Extending with a composition of two injective maps equals a nested extension: extend (f23 ∘ f12) g e' = extend f23 (extend f12 g (e' ∘ f23)) e'.
Русский
Расширение через композицию двух инъективных отображений эквивалентно вложенному расширению: extend (f23 ∘ f12) g e' = extend f23 (extend f12 g (e' ∘ f23)) e'.
LaTeX
$$$\operatorname{extend} (f_{23} \circ f_{12})\ g\ e' = \operatorname{extend} f_{23} (\operatorname{extend} f_{12} g (e' \circ f_{23})) e'$$$
Lean4
theorem extend_comp {α₁ α₂ α₃ : Sort*} {f₁₂ : α₁ → α₂} (h₁₂ : Function.Injective f₁₂) {f₂₃ : α₂ → α₃}
(h₂₃ : Function.Injective f₂₃) (g : α₁ → γ) (e' : α₃ → γ) :
extend (f₂₃ ∘ f₁₂) g e' = extend f₂₃ (extend f₁₂ g (e' ∘ f₂₃)) e' :=
by
ext a
by_cases h₃ : ∃ b, f₂₃ b = a
· obtain ⟨b, rfl⟩ := h₃
rw [Injective.extend_apply h₂₃]
by_cases h₂ : ∃ c, f₁₂ c = b
· obtain ⟨c, rfl⟩ := h₂
rw [h₁₂.extend_apply]
exact (h₂₃.comp h₁₂).extend_apply _ _ _
· rw [extend_apply' _ _ _ h₂, extend_apply', comp_apply]
exact fun h ↦ h₂ (Exists.casesOn h fun c hc ↦ Exists.intro c (h₂₃ hc))
· rw [extend_apply' _ _ _ h₃, extend_apply']
exact fun h ↦ h₃ (Exists.casesOn h fun c hc ↦ Exists.intro (f₁₂ c) (hc))
