iInf_adj_of_nonempty — Mathlib

English

If ι is nonempty, then (iInf f).Adj a b holds iff ∀ i, (f i).Adj a b.

Русский

Если множество индексов непусто, то (iInf f).Adj a b выполняется тогда, когда для всех i вершины a и b смежны в f(i).

LaTeX

$$[Nonempty ι] {f : ι → G.Subgraph} : (iInf fun i => f i).Adj a b \\iff ∀ i, (f i).Adj a b$$

Lean4

theorem iInf_adj_of_nonempty [Nonempty ι] {f : ι → G.Subgraph} : (⨅ i, f i).Adj a b ↔ ∀ i, (f i).Adj a b :=
  by
  rw [iInf, sInf_adj_of_nonempty (Set.range_nonempty _)]
  simp

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