instLocallyFiniteOrder — Mathlib

English

If t is supported on s, membership in s.dfinsupp t is equivalent to pointwise membership in t(i) for all i.

Русский

Если t поддержан на s, принадлежность s.dfinsupp t эквивалентна тому, что для всех i выполняется f(i) ∈ t(i).

LaTeX

$$mem_dfinsupp_iff_of_support_subset {t : Π₀ i, Finset (α i)} (ht : t.support ⊆ s) : f ∈ s.dfinsupp t ↔ ∀ i, f i ∈ t i$$

Lean4

instance instLocallyFiniteOrder : LocallyFiniteOrder (Π₀ i, α i) :=
  LocallyFiniteOrder.ofIcc (Π₀ i, α i) (fun f g => (f.support ∪ g.support).dfinsupp <| f.rangeIcc g)
    (fun f g x => by
      refine (mem_dfinsupp_iff_of_support_subset <| support_rangeIcc_subset).trans ?_
      simp_rw [mem_rangeIcc_apply_iff, forall_and]
      rfl)

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