image_out — Mathlib

English

For any set C of components, the image under Quot.out of C represents C.

Русский

Для любой множества компонент C образ под Quot.out представляет C.

LaTeX

$$$ Represents (Quot.out '' C) C $$$

Lean4

theorem image_out (C : Set G.ConnectedComponent) : Represents (Quot.out '' C) C :=
  Set.BijOn.mk (by rintro c ⟨x, ⟨hx, rfl⟩⟩; simp_all [connectedComponentMk])
    (by
      rintro x ⟨c, ⟨hc, rfl⟩⟩ y ⟨d, ⟨hd, rfl⟩⟩ hxy
      simp only [connectedComponentMk] at hxy
      aesop)
    (fun _ _ ↦ by simpa [connectedComponentMk])

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