instIsFilteredOrEmptyForall — Mathlib

English

If every I(i) is IsFilteredOrEmpty, then the product ∀i I(i) is IsFilteredOrEmpty.

Русский

Если каждый I(i) имеет свойство IsFilteredOrEmpty, то ∀i I(i) имеет это свойство.

LaTeX

$$$\\bigl(\\forall i, \\mathrm{IsFilteredOrEmpty}(I(i))\\bigr) \\Rightarrow \\mathrm{IsFilteredOrEmpty}(\\forall i, I(i))$$$

Lean4

instance [∀ i, IsFilteredOrEmpty (I i)] : IsFilteredOrEmpty (∀ i, I i)
    where
  cocone_objs k
    l := ⟨fun s => max (k s) (l s), fun s => leftToMax (k s) (l s), fun s => rightToMax (k s) (l s), trivial⟩
  cocone_maps k l f
    g := ⟨fun s => coeq (f s) (g s), fun s => coeqHom (f s) (g s), funext fun s => by simp [coeq_condition (f s) (g s)]⟩

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