English
The insertion map is an order-preserving embedding; membership is preserved under the map.
Русский
Отображение вставки сохраняет порядок и сохранение принадлежности подмножества под действием отображения.
LaTeX
$$$ insertTop(s) = \top \cup \{ \operatorname{coe}(a) : a \in s\} $ и выражения о сохранении подмножеств.$$
Lean4
instance locallyFiniteOrder : LocallyFiniteOrder (WithTop α)
where
finsetIcc a
b :=
match a, b with
| ⊤, ⊤ => {⊤}
| ⊤, (b : α) => ∅
| (a : α), ⊤ => insertTop (Ici a)
| (a : α), (b : α) => (Icc a b).map Embedding.coeWithTop
finsetIco a
b :=
match a, b with
| ⊤, _ => ∅
| (a : α), ⊤ => (Ici a).map Embedding.coeWithTop
| (a : α), (b : α) => (Ico a b).map Embedding.coeWithTop
finsetIoc a
b :=
match a, b with
| ⊤, _ => ∅
| (a : α), ⊤ => insertTop (Ioi a)
| (a : α), (b : α) => (Ioc a b).map Embedding.coeWithTop
finsetIoo a
b :=
match a, b with
| ⊤, _ => ∅
| (a : α), ⊤ => (Ioi a).map Embedding.coeWithTop
| (a : α), (b : α) => (Ioo a b).map Embedding.coeWithTop
finset_mem_Icc a b x := by cases a <;> cases b <;> cases x <;> simp
finset_mem_Ico a b x := by cases a <;> cases b <;> cases x <;> simp
finset_mem_Ioc a b x := by cases a <;> cases b <;> cases x <;> simp
finset_mem_Ioo a b x := by cases a <;> cases b <;> cases x <;> simp
