English
If f is an inducing map and x,y ∈ F, then JoinedIn (f(F)) (f(x)) (f(y)) is equivalent to JoinedIn F x y.
Русский
Если f индуктивно отображает, и x,y ∈ F, то JoinedIn (f(F)) (f(x)) (f(y)) эквивалентно JoinedIn F x y.
LaTeX
$$JoinedIn (Set.image f F) (f x) (f y) ↔ JoinedIn F x y$$
Lean4
theorem joinedIn_image {f : X → Y} (hf : IsInducing f) (hx : x ∈ F) (hy : y ∈ F) :
JoinedIn (f '' F) (f x) (f y) ↔ JoinedIn F x y :=
by
refine ⟨?_, (.map · hf.continuous)⟩
rintro ⟨γ, hγ⟩
choose γ' hγ'F hγ' using hγ
have h₀ : x ⤳ γ' 0 := by rw [← hf.specializes_iff, hγ', γ.source]
have h₁ : γ' 1 ⤳ y := by rw [← hf.specializes_iff, hγ', γ.target]
have h : JoinedIn F (γ' 0) (γ' 1) := by
refine ⟨⟨⟨γ', ?_⟩, rfl, rfl⟩, hγ'F⟩
simpa only [hf.continuous_iff, comp_def, hγ'] using map_continuous γ
exact (h₀.joinedIn hx (hγ'F _)).trans <| h.trans <| h₁.joinedIn (hγ'F _) hy
