mono' — Mathlib

English

If H ≤ H', their vertex sets are equal and H is connected, then H' is connected.

Русский

Если H содержится в H', их множества вершин совпадают и H связен, тогда H' связан.

LaTeX

$$$\forall {H \le H' : G.Subgraph},\ hv : H.verts = H'.verts,\ h : H.Connected \Rightarrow H'.Connected$$$

Lean4

protected theorem mono' {H H' : G.Subgraph} (hle : ∀ v w, H.Adj v w → H'.Adj v w) (hv : H.verts = H'.verts)
    (h : H.Connected) : H'.Connected := by exact h.mono ⟨hv.le, hle⟩ hv

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