sup — Mathlib

English

If H and K are connected and their intersection has nonempty vertex set, then their union is connected.

Русский

Если подграфы H и K связны и их пересечение имеет непустое множество вершин, то их объединение связано.

LaTeX

$$$\text{H, K connected} \land (H \cap K).verts.Nonempty \Rightarrow (H \cup K).Connected$$$

Lean4

protected theorem sup {H K : G.Subgraph} (hH : H.Connected) (hK : K.Connected) (hn : (H ⊓ K).verts.Nonempty) :
    (H ⊔ K).Connected := by
  rw [Subgraph.connected_iff', connected_iff_exists_forall_reachable]
  obtain ⟨u, hu, hu'⟩ := hn
  exists ⟨u, Or.inl hu⟩
  rintro ⟨v, (hv | hv)⟩
  · exact Reachable.map (Subgraph.inclusion (le_sup_left : H ≤ H ⊔ K)) (hH ⟨u, hu⟩ ⟨v, hv⟩)
  · exact Reachable.map (Subgraph.inclusion (le_sup_right : K ≤ H ⊔ K)) (hK ⟨u, hu'⟩ ⟨v, hv⟩)

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