Mathlib.Data.Pi.Interval._auxLemma.3
theorem Mathlib.Data.Pi.Interval._auxLemma.3 :
∀ {ι : Type u} {α : ι → Type v} [inst : (i : ι) → LE (α i)] {x y : (i : ι) → α i}, (x ≤ y) = ∀ (i : ι), x i ≤ y i
This is a theorem about functions and ordering in the mathematical library (Mathlib) of Lean 4. The theorem, denoted as `Mathlib.Data.Pi.Interval._auxLemma.3`, states that for any type `ι` and a function `α : ι → Type v` (which maps elements of `ι` to some type `v`), given an ordering (≤) on the range of `α`, and two functions `x` and `y` of type `(i : ι) → α i`, `x` is less than or equal to `y` if and only if `x i` is less than or equal to `y i` for each `i` in `ι`.
More concisely: For any type `ι` and function `α : ι → Type v` with an ordering on its range, `x` and `y` being functions of type `(i : ι) → α i`, the equality `x ≤ y` holds if and only if `x i ≤ y i` for all `i` in `ι`.
|
Pi.card_Icc
theorem Pi.card_Icc :
∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Fintype ι] [inst_1 : DecidableEq ι]
[inst_2 : (i : ι) → DecidableEq (α i)] [inst_3 : (i : ι) → PartialOrder (α i)]
[inst_4 : (i : ι) → LocallyFiniteOrder (α i)] (a b : (i : ι) → α i),
(Finset.Icc a b).card = Finset.univ.prod fun i => (Finset.Icc (a i) (b i)).card
The theorem `Pi.card_Icc` states that for every finite type `ι`, and for every function `α` mapping `ι` to some type, given that `ι` has decidable equality, and for each `i` in `ι`, the `α i` has decidable equality and partial order and locally finite order, then for any two functions `a` and `b` from `ι` to `α`, the cardinality of the finite set `Finset.Icc a b` equals the product of the cardinalities of the finite sets `Finset.Icc (a i) (b i)` for all `i` in the universal finite set of type `Finset ι`.
In simpler terms, it says that the size of the finite interval (inclusive) between two functions is equal to the product of the sizes of the individual intervals (inclusive) for each element of the domain.
More concisely: For every finite type `ι` and function `α : ι → Type`, if `ι` has decidable equality and for each `i` in `ι`, `α i` has decidable equality and partial order with locally finite order, then the cardinality of `Finset.Icc (α a) (α b)` equals the product of the cardinalities of `Finset.Icc (α i) (α i)` for all `i` in `ι`.
|
Mathlib.Data.Pi.Interval._auxLemma.1
theorem Mathlib.Data.Pi.Interval._auxLemma.1 :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {δ : α → Type u_3} {t : (a : α) → Finset (δ a)}
{f : (a : α) → δ a}, (f ∈ Fintype.piFinset t) = ∀ (a : α), f a ∈ t a
The theorem `Mathlib.Data.Pi.Interval._auxLemma.1` states that for any type `α` with decidable equality and finite number of instances, and for any function `δ` from `α` to another type, given a function `t` that maps each instance of type `α` to a finite set of instances of the type determined by `δ`, and a function `f` that maps each instance of `α` to an instance of the type determined by `δ`, the condition `f` being an element of the set of functions from `α` to the types determined by `δ` that are constrained by `t` is equivalent to the condition that for every instance of `α`, the value of `f` at that instance is an element of the set determined by `t` at that instance.
More concisely: For a decidably equal and finite type α, function δ : α -> Type, functions t : α -> Set (δ α), and f : α -> δ α, the condition that for all x : α, f(x) ∈ t(x) is equivalent to f ∈ {g : α -> δ α | ∀ x, g(x) ∈ t(x)} (the set of functions from α to the types determined by δ that are constrained by t).
|