instPreorder — Mathlib

English

A family of ordered sets indexed by α yields a pointwise preorder on the dependent finitely supported functions: f ≤ g iff for all a, f(a) ≤ g(a).

Русский

Для семейства упорядоченных по α множеств образуется поко-упорядочение по координатам: f ≤ g тогда и только если для всех a верно f(a) ≤ g(a).

LaTeX

$$$ f \le g \iff \forall a, f(a) \le g(a) $$$

Lean4

instance : Preorder (Π₀ i, α i) :=
  { (inferInstance : LE (DFinsupp α)) with
    le_refl := fun _ _ ↦ le_rfl
    le_trans := fun _ _ _ hfg hgh i ↦ (hfg i).trans (hgh i) }

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