ordConnected_iInter — Mathlib

English

If every s i in a family {s i} is OrdConnected, then the indexed intersection ∩ i, s i is OrdConnected.

Русский

Если каждый s i в семье {s i} является OrdConnected, то пересечение по i, ∩ i s i является OrdConnected.

LaTeX

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

Lean4

theorem ordConnected_iInter {ι : Sort*} {s : ι → Set α} (hs : ∀ i, OrdConnected (s i)) : OrdConnected (⋂ i, s i) :=
  ordConnected_sInter <| forall_mem_range.2 hs

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