joinedIn_iff_joined — Mathlib

English

Let x,y ∈ F with proofs hx, hy of membership. Then x and y are joined in F iff the corresponding points (x, hx) and (y, hy) are joined in the subtype F.

Русский

Пусть x,y ∈ F и имеются доказательства того, что x, y ∈ F. Тогда x и y соединены в F тогда и только тогда, когда соответствующие точки (x, hx) и (y, hy) соединены в подмножестве F.

LaTeX

$$JoinedIn F x y ⇔ Joined ⟨x, hx⟩ ⟨y, hy⟩$$

Lean4

theorem joinedIn_iff_joined (x_in : x ∈ F) (y_in : y ∈ F) : JoinedIn F x y ↔ Joined (⟨x, x_in⟩ : F) (⟨y, y_in⟩ : F) :=
  ⟨fun h => h.joined_subtype, fun h => ⟨h.somePath.map continuous_subtype_val, by simp⟩⟩

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