instIsCofilteredOrEmptyForall — Mathlib

English

If every I(i) is IsCofilteredOrEmpty, then ∀i I(i) is IsCofilteredOrEmpty.

Русский

Если каждый I(i) кофильтрован или пуст, то ∀i I(i) кофильтрована или пуста.

LaTeX

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

Lean4

instance [∀ i, IsCofilteredOrEmpty (I i)] : IsCofilteredOrEmpty (∀ i, I i)
    where
  cone_objs k l := ⟨fun s => min (k s) (l s), fun s => minToLeft (k s) (l s), fun s => minToRight (k s) (l s), trivial⟩
  cone_maps k l f
    g := ⟨fun s => eq (f s) (g s), fun s => eqHom (f s) (g s), funext fun s => by simp [eq_condition (f s) (g s)]⟩

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