instLocallyFiniteOrder — Mathlib

English

Given a predicate p on α and LocallyFiniteOrder on α, the subtype {x ∈ α | p x} inherits LocallyFiniteOrder via the obvious finite-interval constructions: Icc, Ico, Ioc, Ioo on a,b in Subtype p are just the corresponding interval sets in α restricted to p.

Русский

С заданием предиката p на α и локально конечного порядка на α, подтип {x ∈ α | p x} наследует локально конечный порядок через обычные конечные интервалы: Icc, Ico, Ioc, Ioo для a,b в Subtype p — это соответствующие интервальные множества в α, ограниченные условием p.

LaTeX

$$$$ \\text{Icc}(a,b) = (\\mathrm{Icc}(a.\\mathrm{val}, b.\\mathrm{val})).\\mathrm{subtype}\\ p, \\text{ и т.д.} $$$$

Lean4

instance instLocallyFiniteOrder [LocallyFiniteOrder α] : LocallyFiniteOrder (Subtype p)
    where
  finsetIcc a b := (Icc (a : α) b).subtype p
  finsetIco a b := (Ico (a : α) b).subtype p
  finsetIoc a b := (Ioc (a : α) b).subtype p
  finsetIoo a b := (Ioo (a : α) b).subtype p
  finset_mem_Icc a b x := by simp_rw [Finset.mem_subtype, mem_Icc, Subtype.coe_le_coe]
  finset_mem_Ico a b x := by simp_rw [Finset.mem_subtype, mem_Ico, Subtype.coe_le_coe, Subtype.coe_lt_coe]
  finset_mem_Ioc a b x := by simp_rw [Finset.mem_subtype, mem_Ioc, Subtype.coe_le_coe, Subtype.coe_lt_coe]
  finset_mem_Ioo a b x := by simp_rw [Finset.mem_subtype, mem_Ioo, Subtype.coe_lt_coe]

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