ordConnected_biInter — Mathlib

English

If for all i and hi, OrdConnected (s i hi), then the bi-indexed intersection ⋂ i (hi), s i hi is OrdConnected.

Русский

Если для каждого i и hi выполняется OrdConnected (s i hi), то двоично-интервалное пересечение ⋂ i hi s i hi OrdConnected.

LaTeX

$$$\left( \forall i hi, \operatorname{OrdConnected}(s i hi) \right) \Rightarrow \operatorname{OrdConnected}\left( \bigcap_i \bigcap_{hi} s i hi \right)$$$

Lean4

theorem ordConnected_biInter {ι : Sort*} {p : ι → Prop} {s : ∀ i, p i → Set α} (hs : ∀ i hi, OrdConnected (s i hi)) :
    OrdConnected (⋂ (i) (hi), s i hi) :=
  ordConnected_iInter fun i => ordConnected_iInter <| hs i

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