ordConnected_pi — Mathlib

English

If for all i in s, t i is OrdConnected, then the Pi-type set s.pi t is OrdConnected.

Русский

Если для каждого i из s множество t i является OrdConnected, то множество s.pi t тождественно OrdConnected.

LaTeX

$$$\left( \forall i \in s, \operatorname{OrdConnected}(t i) \right) \Rightarrow \operatorname{OrdConnected}(s \pi t)$$$

Lean4

theorem ordConnected_pi {ι : Type*} {α : ι → Type*} [∀ i, Preorder (α i)] {s : Set ι} {t : ∀ i, Set (α i)}
    (h : ∀ i ∈ s, OrdConnected (t i)) : OrdConnected (s.pi t) :=
  ⟨fun _ hx _ hy _ hz i hi => (h i hi).out (hx i hi) (hy i hi) ⟨hz.1 i, hz.2 i⟩⟩

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