English
Assume LocallyFiniteOrderTop on each αi. Then the Sigma-type Σi, αi inherits LocallyFiniteOrderTop, with finsetIci(⟨i,a⟩) = (Ici a).map (Embedding.sigmaMk i) and finsetIoi(⟨i,a⟩) = (Ioi a).map (Embedding.sigmaMk i), along with the corresponding membership criteria.
Русский
Пусть для каждого αi задан LocallyFiniteOrderTop. Тогда Sigma-тип Σi, αi имеет LocallyFiniteOrderTop, с finsetIci(⟨i,a⟩)=(Ici a).map(Embedding.sigmaMk i) и finsetIoi(⟨i,a⟩)=(Ioi a).map(Embedding.sigmaMk i), а также соответствующие условия принадлежности.
LaTeX
$$$\\operatorname{LocallyFiniteOrderTop}(\\Sigma i,\\alpha i)\\;\\text{with}\\;\\operatorname{finsetIci}(\\langle i,a\\rangle)=(\\operatorname{Ici} a).\\operatorname{map}(\\operatorname{Embedding.sigmaMk} i),\\;\\operatorname{finsetIoi}(\\langle i,a\\rangle)=(\\operatorname{Ioi} a).\\operatorname{map}(\\operatorname{Embedding.sigmaMk} i).$$$
Lean4
instance instLocallyFiniteOrderTop : LocallyFiniteOrderTop (Σ i, α i)
where
finsetIci
| ⟨i, a⟩ => (Ici a).map (Embedding.sigmaMk i)
finsetIoi
| ⟨i, a⟩ => (Ioi a).map (Embedding.sigmaMk i)
finset_mem_Ici := fun ⟨i, a⟩ ⟨j, b⟩ => by
obtain rfl | hij := eq_or_ne i j
· simp
· simp [hij, le_def]
finset_mem_Ioi := fun ⟨i, a⟩ ⟨j, b⟩ => by
obtain rfl | hij := eq_or_ne i j
· simp
· simp [hij, lt_def]
