class FiniteRange {Ω : Type u_1} {G : Type u_2} (X : Ω → G) : Prop

The property of having a finite range.

• finite : (Set.range X).Finite

theorem FiniteRange.finite {Ω : Type u_1} {G : Type u_2} {X : Ω → G} [self : FiniteRange X] : (Set.range X).Finite

noncomputable def FiniteRange.fintype {Ω : Type u_1} {G : Type u_2} (X : Ω → G) [hX : FiniteRange X] : Fintype ↑(Set.range X)

fintype structure on the range of a finite range map.

Equations

• FiniteRange.fintype X = ⋯.fintype

noncomputable def FiniteRange.toFinset {Ω : Type u_1} {G : Type u_2} (X : Ω → G) [hX : FiniteRange X] : Finset G

The range of a finite range map, as a finset.

Equations

• FiniteRange.toFinset X = (Set.range X).toFinset

instance instFiniteRangeOfFintype {Ω : Type u_1} {G : Type u_2} (X : Ω → G) [Fintype G] : FiniteRange X

If the codomain of X is finite, then X has finite range.

Equations

• ⋯ = ⋯

theorem finiteRange_of_finset {Ω : Type u_1} {G : Type u_2} (f : Ω → G) (A : Finset G) (h : ∀ (ω : Ω), f ω ∈ A) : FiniteRange f

Functions ranging in a Finset have finite range

theorem FiniteRange.range {Ω : Type u_1} {G : Type u_2} (X : Ω → G) [hX : FiniteRange X] : Set.range X = ↑(FiniteRange.toFinset X)

theorem FiniteRange.mem {Ω : Type u_1} {G : Type u_2} (X : Ω → G) [FiniteRange X] (ω : Ω) : X ω ∈ FiniteRange.toFinset X

@[simp]

theorem FiniteRange.mem_iff {Ω : Type u_1} {G : Type u_2} (X : Ω → G) [FiniteRange X] (x : G) : x ∈ FiniteRange.toFinset X ↔ ∃ (ω : Ω), X ω = x

instance instFiniteRange {Ω : Type u_1} {G : Type u_2} (c : G) : FiniteRange fun (x : Ω) => c

Constants have finite range

Equations

• ⋯ = ⋯

instance instFiniteRangeComp {Ω : Type u_1} {G : Type u_2} {H : Type u_3} (X : Ω → G) (f : G → H) [hX : FiniteRange X] : FiniteRange (f ∘ X)

If X has finite range, then any function of X has finite range.

Equations

• ⋯ = ⋯

instance instFiniteRangeComp_1 {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_3} (X : Ω → G) (f : Ω' → Ω) [hX : FiniteRange X] : FiniteRange (X ∘ f)

If X has finite range, then X of any function has finite range.

Equations

• ⋯ = ⋯

instance instFiniteRangeProdProd {Ω : Type u_1} {G : Type u_2} {H : Type u_3} (X : Ω → G) (Y : Ω → H) [hX : FiniteRange X] [hY : FiniteRange Y] : FiniteRange (⟨X, Y⟩)

If X, Y have finite range, then so does the pair ⟨X, Y⟩.

Equations

• ⋯ = ⋯

instance FiniteRange.sum {Ω : Type u_1} {G : Type u_2} (X : Ω → G) (Y : Ω → G) [Add G] [hX : FiniteRange X] [hY : FiniteRange Y] : FiniteRange (X + Y)

The sum of functions of finite range, has finite range.

Equations

• ⋯ = ⋯

instance FiniteRange.prod {Ω : Type u_1} {G : Type u_2} (X : Ω → G) (Y : Ω → G) [Mul G] [hX : FiniteRange X] [hY : FiniteRange Y] : FiniteRange (X * Y)

The product of functions of finite range, has finite range.

Equations

• ⋯ = ⋯

instance FiniteRange.sub {Ω : Type u_1} {G : Type u_2} (X : Ω → G) (Y : Ω → G) [Sub G] [hX : FiniteRange X] [hY : FiniteRange Y] : FiniteRange (X - Y)

The difference of functions of finite range, has finite range.

Equations

• ⋯ = ⋯

instance FiniteRange.div {Ω : Type u_1} {G : Type u_2} (X : Ω → G) (Y : Ω → G) [Div G] [hX : FiniteRange X] [hY : FiniteRange Y] : FiniteRange (X / Y)

The quotient of two functions with finite range, has finite range.

Equations

• ⋯ = ⋯

instance FiniteRange.neg {Ω : Type u_1} {G : Type u_2} (X : Ω → G) [Neg G] [hX : FiniteRange X] : FiniteRange (-X)

The negation of a function of finite range, has finite range.

Equations

• ⋯ = ⋯

instance FiniteRange.inv {Ω : Type u_1} {G : Type u_2} (X : Ω → G) [Inv G] [hX : FiniteRange X] : FiniteRange X⁻¹

The inverse of a function of finite range, has finite range.

Equations

• ⋯ = ⋯

instance FiniteRange.nsmul {Ω : Type u_1} {G : Type u_2} (X : Ω → G) [SMul ℤ G] [hX : FiniteRange X] (c : ℤ) : FiniteRange (c • X)

The multiple of a function of finite range by a constant, has finite range.

Equations

• ⋯ = ⋯

instance FiniteRange.pow {Ω : Type u_1} {G : Type u_2} (X : Ω → G) [Pow G ℤ] [hX : FiniteRange X] (c : ℤ) : FiniteRange (X ^ c)

A function of finite range raised to a constant power, has finite range.

Equations

• ⋯ = ⋯

instance FiniteRange.finsum {Ω : Type u_1} {G : Type u_2} {I : Type u_3} [AddCommMonoid G] {s : Finset I} (X : I → Ω → G) [∀ (i : I), FiniteRange (X i)] : FiniteRange (s.sum fun (i : I) => X i)

The sum of a finite number of functions with finite range, has finite range.

Equations

• ⋯ = ⋯

instance FiniteRange.finprod {Ω : Type u_1} {G : Type u_2} {I : Type u_3} [CommMonoid G] {s : Finset I} (X : I → Ω → G) [∀ (i : I), FiniteRange (X i)] : FiniteRange (s.prod fun (i : I) => X i)

The product of a finite number of functions with finite range, has finite range.

Equations

• ⋯ = ⋯

theorem FiniteRange.full {Ω : Type u_1} {G : Type u_2} [MeasurableSpace Ω] [MeasurableSpace G] [MeasurableSingletonClass G] {X : Ω → G} (hX : Measurable X) [FiniteRange X] (μ : MeasureTheory.Measure Ω) : (MeasureTheory.Measure.map X μ) ↑(FiniteRange.toFinset X) = μ Set.univ

theorem FiniteRange.null_of_compl {Ω : Type u_1} {G : Type u_2} [MeasurableSpace Ω] [MeasurableSpace G] [MeasurableSingletonClass G] (μ : MeasureTheory.Measure Ω) (X : Ω → G) [FiniteRange X] : (MeasureTheory.Measure.map X μ) (↑(FiniteRange.toFinset X))ᶜ = 0