English
The open down-interval below b, Iio b, is finite in a locally finite order with a bottom.
Русский
Убывательный открытый интервал ниже b, Iio b, конечен в локально конченном порядка с нижней границей.
LaTeX
$$$\forall b \in \alpha, \lvert \{ x \in \alpha \mid x < b \} \rvert < \infty$$$
Lean4
/-- Given an order embedding `α ↪o β`, pulls back the `LocallyFiniteOrder` on `β` to `α`. -/
protected noncomputable def locallyFiniteOrder [LocallyFiniteOrder β] (f : α ↪o β) : LocallyFiniteOrder α
where
finsetIcc a b := (Icc (f a) (f b)).preimage f f.toEmbedding.injective.injOn
finsetIco a b := (Ico (f a) (f b)).preimage f f.toEmbedding.injective.injOn
finsetIoc a b := (Ioc (f a) (f b)).preimage f f.toEmbedding.injective.injOn
finsetIoo a b := (Ioo (f a) (f b)).preimage f f.toEmbedding.injective.injOn
finset_mem_Icc a b x := by rw [mem_preimage, mem_Icc, f.le_iff_le, f.le_iff_le]
finset_mem_Ico a b x := by rw [mem_preimage, mem_Ico, f.le_iff_le, f.lt_iff_lt]
finset_mem_Ioc a b x := by rw [mem_preimage, mem_Ioc, f.lt_iff_lt, f.le_iff_le]
finset_mem_Ioo a b x := by rw [mem_preimage, mem_Ioo, f.lt_iff_lt, f.lt_iff_lt]
