Documentation

Mathlib.Data.DFinsupp.Interval

Finite intervals of finitely supported functions #

This file provides the LocallyFiniteOrder instance for Π₀ i, α i when α itself is locally finite and calculates the cardinality of its finite intervals.

source
def Finset.dfinsupp {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → Zero (α i)] (s : Finset ι) (t : (i : ι) → Finset (α i)) :
Finset (Π₀ (i : ι), α i)

Finitely supported product of finsets.

Equations
    Instances For
      source
      @[simp]
      theorem Finset.card_dfinsupp {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → Zero (α i)] (s : Finset ι) (t : (i : ι) → Finset (α i)) :
      (s.dfinsupp t).card = ∏ i ∈ s, (t i).card
      source
      theorem Finset.mem_dfinsupp_iff {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → Zero (α i)] {s : Finset ι} {f : Π₀ (i : ι), α i} {t : (i : ι) → Finset (α i)} [(i : ι) → DecidableEq (α i)] :
      f ∈ s.dfinsupp t ↔ f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i
      source
      @[simp]
      theorem Finset.mem_dfinsupp_iff_of_support_subset {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → Zero (α i)] {s : Finset ι} {f : Π₀ (i : ι), α i} [(i : ι) → DecidableEq (α i)] {t : Π₀ (i : ι), Finset (α i)} (ht : t.support ⊆ s) :
      f ∈ s.dfinsupp ⇑t ↔ ∀ (i : ι), f i ∈ t i

      When t is supported on s, f ∈ s.dfinsupp t precisely means that f is pointwise in t.

      source
      def DFinsupp.singleton {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] (f : Π₀ (i : ι), α i) :
      Π₀ (i : ι), Finset (α i)

      Pointwise Finset.singleton bundled as a DFinsupp.

      Equations
        Instances For
          source
          theorem DFinsupp.mem_singleton_apply_iff {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] {f : Π₀ (i : ι), α i} {i : ι} {a : α i} :
          a ∈ f.singleton i ↔ a = f i
          source
          def DFinsupp.rangeIcc {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f g : Π₀ (i : ι), α i) :
          Π₀ (i : ι), Finset (α i)

          Pointwise Finset.Icc bundled as a DFinsupp.

          Equations
            Instances For
              source
              @[simp]
              theorem DFinsupp.rangeIcc_apply {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f g : Π₀ (i : ι), α i) (i : ι) :
              (f.rangeIcc g) i = Finset.Icc (f i) (g i)
              source
              theorem DFinsupp.mem_rangeIcc_apply_iff {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] {f g : Π₀ (i : ι), α i} {i : ι} {a : α i} :
              a ∈ (f.rangeIcc g) i ↔ f i ≤ a ∧ a ≤ g i
              source
              theorem DFinsupp.support_rangeIcc_subset {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → LocallyFiniteOrder (α i)] {f g : Π₀ (i : ι), α i} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] :
              (f.rangeIcc g).support ⊆ f.support ∪ g.support
              source
              def DFinsupp.pi {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [DecidableEq ι] [(i : ι) → DecidableEq (α i)] (f : Π₀ (i : ι), Finset (α i)) :
              Finset (Π₀ (i : ι), α i)

              Given a finitely supported function f : Π₀ i, Finset (α i), one can define the finset f.pi of all finitely supported functions whose value at i is in f i for all i.

              Equations
                Instances For
                  source
                  @[simp]
                  theorem DFinsupp.mem_pi {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [DecidableEq ι] [(i : ι) → DecidableEq (α i)] {f : Π₀ (i : ι), Finset (α i)} {g : Π₀ (i : ι), α i} :
                  g ∈ f.pi ↔ ∀ (i : ι), g i ∈ f i
                  source
                  @[simp]
                  theorem DFinsupp.card_pi {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → Zero (α i)] [DecidableEq ι] [(i : ι) → DecidableEq (α i)] (f : Π₀ (i : ι), Finset (α i)) :
                  f.pi.card = f.prod fun (i : ι) => ↑(f i).card
                  source
                  instance DFinsupp.instLocallyFiniteOrder {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] [(i : ι) → LocallyFiniteOrder (α i)] :
                  LocallyFiniteOrder (Π₀ (i : ι), α i)
                  Equations
                    source
                    theorem DFinsupp.Icc_eq {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f g : Π₀ (i : ι), α i) :
                    Finset.Icc f g = (f.support ∪ g.support).dfinsupp ⇑(f.rangeIcc g)
                    source
                    theorem DFinsupp.card_Icc {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f g : Π₀ (i : ι), α i) :
                    (Finset.Icc f g).card = ∏ i ∈ f.support ∪ g.support, (Finset.Icc (f i) (g i)).card
                    source
                    theorem DFinsupp.card_Ico {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f g : Π₀ (i : ι), α i) :
                    (Finset.Ico f g).card = ∏ i ∈ f.support ∪ g.support, (Finset.Icc (f i) (g i)).card - 1
                    source
                    theorem DFinsupp.card_Ioc {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f g : Π₀ (i : ι), α i) :
                    (Finset.Ioc f g).card = ∏ i ∈ f.support ∪ g.support, (Finset.Icc (f i) (g i)).card - 1
                    source
                    theorem DFinsupp.card_Ioo {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → PartialOrder (α i)] [(i : ι) → Zero (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f g : Π₀ (i : ι), α i) :
                    (Finset.Ioo f g).card = ∏ i ∈ f.support ∪ g.support, (Finset.Icc (f i) (g i)).card - 2
                    source
                    theorem DFinsupp.card_uIcc {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → Lattice (α i)] [(i : ι) → Zero (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f g : Π₀ (i : ι), α i) :
                    (Finset.uIcc f g).card = ∏ i ∈ f.support ∪ g.support, (Finset.uIcc (f i) (g i)).card
                    source
                    theorem DFinsupp.card_Iic {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), CanonicallyOrderedAdd (α i)] [(i : ι) → OrderBot (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f : Π₀ (i : ι), α i) :
                    (Finset.Iic f).card = ∏ i ∈ f.support, (Finset.Iic (f i)).card
                    source
                    theorem DFinsupp.card_Iio {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ι] [(i : ι) → DecidableEq (α i)] [(i : ι) → AddCommMonoid (α i)] [(i : ι) → PartialOrder (α i)] [∀ (i : ι), CanonicallyOrderedAdd (α i)] [(i : ι) → OrderBot (α i)] [(i : ι) → LocallyFiniteOrder (α i)] (f : Π₀ (i : ι), α i) :
                    (Finset.Iio f).card = ∏ i ∈ f.support, (Finset.Iic (f i)).card - 1