English
For a predicate p on α with LocallyFiniteOrderTop on α, the subtype p has LocallyFiniteOrderTop with Ici and Ioi given by restricting to p: Ici a = Ici(a.val).subtype p and Ioi a = Ioi(a.val).subtype p.
Русский
Для предиката p на α и LocallyFiniteOrderTop на α подтип p имеет соответствующий LocallyFiniteOrderTop с ограничениями: Ici a = Ici(a.val).subtype p, Ioi a = Ioi(a.val).subtype p.
LaTeX
$$$$ \\mathrm{subtype}\\ p \\;\\text{ имеет } \\mathrm{LocallyFiniteOrderTop} \\text{с } \\mathrm{Ici}, \\mathrm{Ioi} : \\\\ Ici(a) = (Ici(a.\\mathrm{val})).subtype p, \\; Ioi(a) = (Ioi(a.\\mathrm{val})).subtype p. $$$$
Lean4
instance instLocallyFiniteOrderTop [LocallyFiniteOrderTop α] : LocallyFiniteOrderTop (Subtype p)
where
finsetIci a := (Ici (a : α)).subtype p
finsetIoi a := (Ioi (a : α)).subtype p
finset_mem_Ici a x := by simp_rw [Finset.mem_subtype, mem_Ici, Subtype.coe_le_coe]
finset_mem_Ioi a x := by simp_rw [Finset.mem_subtype, mem_Ioi, Subtype.coe_lt_coe]
