English
With a predicate p and LocallyFiniteOrderBot on α, the subtype p inherits LocallyFiniteOrderBot via Iic and Iio: Iic a = (Iic a.val).subtype p and Iio a = (Iio a.val).subtype p.
Русский
При предикате p и LocallyFiniteOrderBot на α подтип p наследует через Iic и Iio: Iic a = (Iic a.val).subtype p, Iio a = (Iio a.val).subtype p.
LaTeX
$$$$ \\mathrm{subtype}\\ p \\;\\text{ имеет } \\mathrm{LocallyFiniteOrderBot} \\text{ с } Iic, Iio. $$$$
Lean4
instance instLocallyFiniteOrderBot [LocallyFiniteOrderBot α] : LocallyFiniteOrderBot (Subtype p)
where
finsetIic a := (Iic (a : α)).subtype p
finsetIio a := (Iio (a : α)).subtype p
finset_mem_Iic a x := by simp_rw [Finset.mem_subtype, mem_Iic, Subtype.coe_le_coe]
finset_mem_Iio a x := by simp_rw [Finset.mem_subtype, mem_Iio, Subtype.coe_lt_coe]
