joinedIn — Mathlib

English

If x specializes to y and x,y ∈ F, then there exists a path in F from x to y.

Русский

Если x специализируется на y и x,y ∈ F, то существует путь в F от x к y.

LaTeX

$$Specializes x y → x ∈ F → y ∈ F → JoinedIn F x y$$

Lean4

theorem joinedIn (h : x ⤳ y) (hx : x ∈ F) (hy : y ∈ F) : JoinedIn F x y :=
  by
  refine ⟨⟨⟨Set.piecewise { 1 } (const I y) (const I x), ?_⟩, by simp, by simp⟩, fun t ↦ ?_⟩
  · exact isClosed_singleton.continuous_piecewise_of_specializes continuous_const continuous_const fun _ ↦ h
  · simp only [Path.coe_mk_mk, piecewise]
    split_ifs <;> assumption

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