exists — Mathlib

English

For any property p on connected components, there exists a connected component with that property if and only if there exists a vertex v such that p holds for the component of v.

Русский

Для любого свойства p, определенного на компонентах связности, существует такая компонента, что свойство выполняется, если и только если существует вершина v такая, что p выполняется для компоненты, заданной вершиной v.

LaTeX

$$$(\\\\exists c : G.ConnectedComponent, p c) \\\\iff \\\\exists v, p (G.connectedComponentMk v)$$$

Lean4

protected theorem «exists» {p : G.ConnectedComponent → Prop} :
    (∃ c : G.ConnectedComponent, p c) ↔ ∃ v, p (G.connectedComponentMk v) :=
  Quot.mk_surjective.exists

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