instLocallyFiniteOrder

Mathlib.Data.Finsupp.Interval

URI: https://scilib.ai/kg/mathlib#Finsupp.instLocallyFiniteOrder

Lean4

instance instLocallyFiniteOrder : LocallyFiniteOrder (ι →₀ α) :=
  LocallyFiniteOrder.ofIcc (ι →₀ α) (fun f g => (f.support ∪ g.support).finsupp <| f.rangeIcc g) fun f g x =>
    by
    refine (mem_finsupp_iff_of_support_subset <| Finset.subset_of_eq <| rangeIcc_support _ _).trans ?_
    simp_rw [mem_rangeIcc_apply_iff]
    exact forall_and

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru