iInf_adj_of_nonempty — Mathlib

English

Same as the previous statement: if ι is nonempty, then (iInf i f(i)).Adj a b ↔ ∀ i, (f i).Adj a b.

Русский

То же самое: если ι непусто, то (iInf_i f(i)).Adj a b эквивалентно ∀ i, (f i).Adj a b.

LaTeX

$$$ (\inf i, f(i)).Adj a b \iff \forall i, (f(i)).Adj a b $$$

Lean4

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

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