iInf_adj — Mathlib

English

Let f be a family of simple graphs on the same vertex set. Then the adjacency in the infimum graph ⨅i f i holds exactly when every graph f i has the edge and the endpoints are distinct: (⨅i, f i).Adj a b iff (∀ i, (f i).Adj a b) ∧ a ≠ b.

Русский

Пусть имеется_family графов на одном наборе вершин; тогда смежность в графе наименьшего элемента ⨅i f i задаётся так: a и b смежны в ⨅i f i тогда и только тогда, когда во всех графах f i есть ребро a—b и a ≠ b.

LaTeX

$$$ (\iInf i, f i).Adj a b \iff (\forall i, (f i).Adj a b) \land a \neq b $$$

Lean4

@[simp]
theorem iInf_adj {f : ι → SimpleGraph V} : (⨅ i, f i).Adj a b ↔ (∀ i, (f i).Adj a b) ∧ a ≠ b := by simp [iInf]

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