forall — Mathlib

English

An isomorphism φ between graphs G and G' induces a bijection between their connected components; the induced map sends each component to the corresponding image component under φ.

Русский

Изоморфизм φ между графами G и G' порождает биекцию между их компонентами связности; полученная отображение отправляет каждую компоненту в соответствующую образующую компоненту под действием φ.

LaTeX

$$$G' .connectedComponentMk (\\\\phi v) = C.map \\\\phi \\\\iff G.connectedComponentMk v = C$$$

Lean4

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

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