ordConnected_iInter' — Mathlib

English

An instance: if every s i is OrdConnected, then the indexed intersection ∩ i, s i is OrdConnected.

Русский

Инстанс: если каждый s i OrdConnected, то индексированная пересечение ∩ i s i OrdConnected.

LaTeX

$$$\left( \forall i, (s i).OrdConnected \right) \Rightarrow (\bigcap_i s_i).OrdConnected$$$

Lean4

instance ordConnected_iInter' {ι : Sort*} {s : ι → Set α} [∀ i, OrdConnected (s i)] : OrdConnected (⋂ i, s i) :=
  ordConnected_iInter ‹_›

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