connectedComponentIn_eq — Mathlib

English

If y ∈ connectedComponentIn F x, then connectedComponentIn F x = connectedComponentIn F y.

Русский

Если y ∈ connectedComponentIn F x, то connectedComponentIn F x = connectedComponentIn F y.

LaTeX

$$$y \in connectedComponentIn F x \Rightarrow connectedComponentIn F x = connectedComponentIn F y$$$

Lean4

theorem connectedComponentIn_eq {x y : α} {F : Set α} (h : y ∈ connectedComponentIn F x) :
    connectedComponentIn F x = connectedComponentIn F y :=
  by
  have hx : x ∈ F := connectedComponentIn_nonempty_iff.mp ⟨y, h⟩
  simp_rw [connectedComponentIn_eq_image hx] at h ⊢
  obtain ⟨⟨y, hy⟩, h2y, rfl⟩ := h
  simp_rw [connectedComponentIn_eq_image hy, connectedComponent_eq h2y]

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