sInf_adj — Mathlib

English

For the infimum of a set s of digraphs, the adjacency relation is true exactly when every member graph contains the edge.

Русский

Для инфимума множества графов отношение смежности истинно тогда и только тогда, когда ребро присутствует во всех графах множества.

LaTeX

$$$(\\mathrm{inf}\\, s).Adj(a,b) \\iff \\forall G\\in s,\\; G.Adj(a,b)$$$

Lean4

@[simp]
theorem sInf_adj {s : Set (Digraph V)} : (sInf s).Adj a b ↔ ∀ G ∈ s, Adj G a b :=
  Iff.rfl

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