joined_subtype — Mathlib

English

If x and y are joined in F, then their images in the subtype F are joined.

Русский

Если x и y соединены в F, то их образы в подпространстве F соединены.

LaTeX

$$$JoinedIn\;(f) \Rightarrow Joined (⟨x, h.source_mem⟩ : F) (⟨y, h.target_mem⟩ : F)$$$

Lean4

/-- If `x` and `y` are joined in the set `F`, then they are joined in the subtype `F`. -/
theorem joined_subtype (h : JoinedIn F x y) : Joined (⟨x, h.source_mem⟩ : F) (⟨y, h.target_mem⟩ : F) :=
  ⟨{  toFun := fun t => ⟨h.somePath t, h.somePath_mem t⟩
      continuous_toFun := by fun_prop
      source' := by simp
      target' := by simp }⟩

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