ordConnected_sInter — Mathlib

English

If every member of a collection S of sets is OrdConnected, then the intersection over all of S is OrdConnected.

Русский

Если каждый элемент семейства S множеств является OrdConnected, то их пересечение ⋂S также OrdConnected.

LaTeX

$$$\left( \forall S \in \mathcal{S},\; \operatorname{OrdConnected}(S) \right) \Rightarrow \operatorname{OrdConnected}\left( \bigcap \mathcal{S} \right)$$$

Lean4

theorem ordConnected_sInter {S : Set (Set α)} (hS : ∀ s ∈ S, OrdConnected s) : OrdConnected (⋂₀ S) :=
  ⟨fun _x hx _y hy _z hz s hs => (hS s hs).out (hx s hs) (hy s hs) hz⟩

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