ordConnected_pi' — Mathlib

English

An instance: if every t i is OrdConnected, then s.pi t is OrdConnected.

Русский

Инстанс: если каждый t i OrdConnected, то s.pi t OrdConnected.

LaTeX

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

Lean4

instance ordConnected_pi' {ι : Type*} {α : ι → Type*} [∀ i, Preorder (α i)] {s : Set ι} {t : ∀ i, Set (α i)}
    [h : ∀ i, OrdConnected (t i)] : OrdConnected (s.pi t) :=
  ordConnected_pi fun i _ => h i

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