sInf_adj_of_nonempty — Mathlib

English

If s is nonempty, then (sInf s).Adj a b holds iff every G' ∈ s satisfies Adj a b.

Русский

Если s непусто, то (sInf s).Adj a b выполняется тогда, когда для каждого G' ∈ s вершины a и b смежны.

LaTeX

$$$ (sInf s).Adj a b \\iff \\forall G' \\in s, Adj\\, G'\\, a\\, b $$$

Lean4

theorem sInf_adj_of_nonempty {s : Set G.Subgraph} (hs : s.Nonempty) : (sInf s).Adj a b ↔ ∀ G' ∈ s, Adj G' a b :=
  sInf_adj.trans <|
    and_iff_left_of_imp <| by
      obtain ⟨G', hG'⟩ := hs
      exact fun h => G'.adj_sub (h _ hG')

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