instLocallyFiniteOrderBot — Mathlib

English

Let (αi)i∈ι be a family of preordered types, each endowed with a locally finite order with bottom. Then the dependent sum Σi, αi carries a LocallyFiniteOrderBot structure, defined coordinatewise by the embedding σMk i: {i} × αi → Σi, αi; in particular finsetIic(⟨i,a⟩) = (Iic a).map (Embedding.sigmaMk i) and finsetIio(⟨i,a⟩) = (Iio a).map (Embedding.sigmaMk i), with the usual finset membership conditions corresponding to these descriptions.

Русский

Пусть (αi)i∈ι — семейство упорядоченных по отношению типов, каждый из которых имеет локально конечный порядок с нижним элементом. Тогда зависимая сумма Σi, αi образует структуру LocallyFiniteOrderBot: финсетfinsetIic(⟨i,a⟩) равен отображению (Iic a) через отображение σMk i, и finsetIio(⟨i,a⟩) равен отображению (Iio a) через σMk i, а согласно определению эти множества описывают подклассы элементов, не превосходящих/близких к a в i-координате.

LaTeX

$$$\\operatorname{LocallyFiniteOrderBot}(\\Sigma i,\\alpha i)\\;\\text{with}\\;\\operatorname{finsetIic}(\\langle i,a\\rangle)=(\\operatorname{Iic} a)\\\\.\\operatorname{map}(\\operatorname{Embedding.sigmaMk} i),\\;\\operatorname{finsetIio}(\\langle i,a\\rangle)=(\\operatorname{Iio} a)\\Catald{ } \\.\\operatorname{map}(\\operatorname{Embedding.sigmaMk} i).$$$

Lean4

instance instLocallyFiniteOrderBot : LocallyFiniteOrderBot (Σ i, α i)
    where
  finsetIic
    | ⟨i, a⟩ => (Iic a).map (Embedding.sigmaMk i)
  finsetIio
    | ⟨i, a⟩ => (Iio a).map (Embedding.sigmaMk i)
  finset_mem_Iic := fun ⟨i, a⟩ ⟨j, b⟩ => by
    obtain rfl | hij := eq_or_ne i j
    · simp
    · simp [hij, le_def, hij.symm]
  finset_mem_Iio := fun ⟨i, a⟩ ⟨j, b⟩ => by
    obtain rfl | hij := eq_or_ne i j
    · simp
    · simp [hij, lt_def, hij.symm]

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