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

The property of having a finite range.

• finite : (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.

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 = ↑(toFinset X)

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

@[simp]

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

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

Constants have finite range

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.

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.

instance instFiniteRangeProdMk {Ω : Type u_1} {G : Type u_2} {H : Type u_3} (X : Ω → G) (Y : Ω → H) [hX : FiniteRange X] [hY : FiniteRange Y] : FiniteRange fun (ω : Ω) => (X ω, Y ω)

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

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

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

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

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

instance FiniteRange.mul' {Ω : Type u_1} {G : Type u_2} (X Y : Ω → G) [Mul G] [FiniteRange X] [FiniteRange Y] : FiniteRange fun (ω : Ω) => X ω * Y ω

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

instance FiniteRange.add' {Ω : Type u_1} {G : Type u_2} (X Y : Ω → G) [Add G] [FiniteRange X] [FiniteRange Y] : FiniteRange fun (ω : Ω) => X ω + Y ω

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

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

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

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

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

instance FiniteRange.div' {Ω : Type u_1} {G : Type u_2} (X Y : Ω → G) [Div G] [FiniteRange X] [FiniteRange Y] : FiniteRange fun (ω : Ω) => X ω / Y ω

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

instance FiniteRange.sub' {Ω : Type u_1} {G : Type u_2} (X Y : Ω → G) [Sub G] [FiniteRange X] [FiniteRange Y] : FiniteRange fun (ω : Ω) => X ω - Y ω

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

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.

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.

instance FiniteRange.inv' {Ω : Type u_1} {G : Type u_2} (X : Ω → G) [Inv G] [FiniteRange X] : FiniteRange fun (ω : Ω) => (X ω)⁻¹

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

instance FiniteRange.neg' {Ω : Type u_1} {G : Type u_2} (X : Ω → G) [Neg G] [FiniteRange X] : FiniteRange fun (ω : Ω) => -X ω

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

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

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

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

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

instance FiniteRange.zpow' {Ω : Type u_1} {G : Type u_2} (X : Ω → G) [Pow G ℤ] [FiniteRange X] (n : ℤ) : FiniteRange fun (ω : Ω) => X ω ^ n

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

instance FiniteRange.zsmul' {Ω : Type u_1} {G : Type u_2} (X : Ω → G) [SMul ℤ G] [FiniteRange X] (n : ℤ) : FiniteRange fun (ω : Ω) => n • X ω

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

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 (∏ i ∈ s, X i)

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

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 (∑ i ∈ s, X i)

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

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 μ) ↑(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 μ) (↑(toFinset X))ᶜ = 0