DFunLike.ext'
theorem DFunLike.ext' :
∀ {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] {f g : F}, ⇑f = ⇑g → f = g
This theorem states that for any dependent function-like type `F` with a domain `α` and a codomain that depends on `α,` denoted as `β : α → Sort u_3`, if we have two instances `f` and `g` of this type `F`, and their function applications (represented by the coercion to a function, `⇑f` and `⇑g`) are equal, then `f` and `g` themselves are equal. Essentially, it asserts the extensionality of dependent function-like objects.
More concisely: If `F` is a dependent function-like type with domain `α` and codomain `β : α → Sort u_3`, and `⇑f = ⇑g` for `f, g : F α`, then `f = g`.
|
DFunLike.ext_iff
theorem DFunLike.ext_iff :
∀ {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] {f g : F}, f = g ↔ ∀ (x : α), f x = g x
This theorem, `DFunLike.ext_iff`, states that for any two dependent function-like structures `f` and `g` of type `F`, with `α` as the input sort and `β` as the function from `α` to a sort `u_3`, they are equal if and only if they return the same output for every input `x` of type `α`. This is a fundamental property of function-like structures in type theory, encapsulating a version of the 'extensionality' axiom for dependent functions.
More concisely: Two dependent function-like structures of type `F` with input sort `α` and output sort `u_3`, `f` and `g`, are equal if and only if for all `x` of type `α`, `f x = g x`.
|
DFunLike.congr_fun
theorem DFunLike.congr_fun :
∀ {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] {f g : F}, f = g → ∀ (x : α), f x = g x
This theorem, named `DFunLike.congr_fun`, states that for any dependent function-like `F` from `α` to `β`, given `f` and `g` are two instances of `F`, if `f` is equal to `g`, then the results of applying `f` and `g` to any element `x` of `α` are also equal. This ensures the congruence property of dependent function-like structures.
More concisely: For any dependent function-like `F` from `α` to `β` and `x` in `α`, if `F.app f x` equals `F.app g x` for all `f` and `g` instances of `F`, then `f` equals `g`.
|
DFunLike.coe_injective'
theorem DFunLike.coe_injective' :
∀ {F : Sort u_1} {α : outParam (Sort u_2)} {β : outParam (α → Sort u_3)} [self : DFunLike F α β],
Function.Injective DFunLike.coe
The theorem `DFunLike.coe_injective'` states that for any sort `F`, output parameter sorts `α` and `β`, where `β` is dependent on `α`, and any instance `self` of `DFunLike F α β`, the function `DFunLike.coe` is injective. This means that, for any two instances of `F`, if applying `DFunLike.coe` to these instances produces the same result, then the two instances must have been the same to begin with.
More concisely: For any sort `F`, given instances `self1 : DFunLike F α β` and `self2 : DFunLike F α β`, if `DFunLike.coe self1 = DFunLike.coe self2`, then `self1 = self2`.
|
DFunLike.ext
theorem DFunLike.ext :
∀ {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] (f g : F), (∀ (x : α), f x = g x) → f = g
This theorem states that for any type `F` of a certain sort `u_1`, any type `α` of a certain sort `u_2`, and any function `β` from `α` to a certain sort `u_3` such that `F` is like a dependent function from `α` to `β` (as denoted by the `DFunLike F α β` instance `i`), if two elements `f` and `g` of `F` are the same for all values of type `α` (i.e., `f x = g x` for all `x` in `α`), then `f` and `g` must actually be the same, or in other words `f = g`.
More concisely: If `F` is a dependent function type from `α` to `β` and `f` and `g` are elements of `F` such that `f x = g x` for all `x` in `α`, then `f = g`.
|
Mathlib.Data.FunLike.Basic._auxLemma.1
theorem Mathlib.Data.FunLike.Basic._auxLemma.1 :
∀ {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] {f g : F}, (⇑f = ⇑g) = (f = g)
This theorem, from the Mathlib library in Lean, states that for any sorts `F`, `α`, and `β`(where `β` is dependent on `α`), and for any `i` which is an instance of the typeclass `DFunLike` over `F`, `α` and `β`, then for any two objects `f` and `g` of sort `F`, the statement that the function-application of `f` is equal to the function-application of `g` is equivalent to saying that `f` is equal to `g`. Essentially, this theorem asserts that two functional-like objects are equal if and only if their corresponding function-applications are equal.
More concisely: For any sorts `F`, `α`, and `β` (with `β` dependent on `α`), and for any `i` an instance of `DFunLike` over `F`, `α`, and `β`, two objects `f` and `g` of sort `F` are equal if and only if `f α = g α` for all `α`.
|
DFunLike.ext'_iff
theorem DFunLike.ext'_iff :
∀ {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] {f g : F}, f = g ↔ ⇑f = ⇑g
This theorem states that for any two functions `f` and `g` of a type `F` that behaves like a dependent function (this behavior is captured by `DFunLike F α β`), `f` is equal to `g` if and only if the application of `f` and `g` to any arguments yield the same results. Here, `α` is the sort of the argument, `β` is a function from `α` to a sort, defining the result type of the function depending on the argument, and `F` is a sort that behaves like such a dependent function. In other words, two such dependent functions are identical if they produce the same output for every possible input.
More concisely: For functions `f` and `g` of sort `F` with dependent types `α` and `β`, `f = g` if and only if `f α = g α` for all `α`.
|
DFunLike.subsingleton_cod
theorem DFunLike.subsingleton_cod :
∀ {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] [inst : ∀ (a : α), Subsingleton (β a)],
Subsingleton F
The theorem `DFunLike.subsingleton_cod` states that for any sort `F` and for any two sorts `α` and `β` where `β` is a dependent function of `α`, if `F` behaves like a dependent function from `α` to `β` (i.e., `F` is a `DFunLike` object from `α` to `β`), and if for every element `a` of `α` the sort `β a` is a subsingleton, then `F` is also a subsingleton. A subsingleton is a type or sort with at most one element. This theorem essentially asserts that if each `β a` is a subsingleton, then any "function-like" object mapping from `α` to `β a` is also a subsingleton.
More concisely: If `F` is a `DFunLike` object from a sort `α` to a subsingleton sort `β`, which is a dependent function of `α`, then `F` is a subsingleton.
|
DFunLike.ne_iff
theorem DFunLike.ne_iff :
∀ {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] {f g : F}, f ≠ g ↔ ∃ a, f a ≠ g a := by
sorry
This theorem states that for any type `F` that behaves like a dependent function (as specified by the `DFunLike F α β` typeclass) from a type `α` to a type `β` dependent on `α`, two such "functions" `f` and `g` are not equal if and only if there exists an element `a` of type `α` such that `f a` is not equal to `g a`. In other words, two dependent function-like objects are different if and only if they differ on at least one input.
More concisely: For any dependent function-like types `F α β` and functions `f` and `g` of type `F α β`, if `a` is an element of `α` such that `f a ≠ g a`, then `f ≠ g`.
|
DFunLike.congr_arg
theorem DFunLike.congr_arg :
∀ {F : Sort u_1} {α : Sort u_2} {β : Sort u_3} [i : FunLike F α β] (f : F) {x y : α}, x = y → f x = f y
The theorem `DFunLike.congr_arg` states that for all types `F`, `α`, and `β`, where `F` is a type that behaves like a function from `α` to `β` (as defined by the `FunLike` class), for any function-like `f` of type `F` and for any two elements `x` and `y` of type `α`, if `x` equals `y`, then the result of applying `f` to `x` equals the result of applying `f` to `y`. This theorem essentially captures the property of a function that equal inputs yield equal outputs.
More concisely: For any `FunLike F α β`, if `x = y : α`, then `F.app f x = F.app f y : β`.
|
DFunLike.coe_injective
theorem DFunLike.coe_injective :
∀ {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β], Function.Injective fun f => ⇑f
The theorem `DFunLike.coe_injective` states that for any sort `F`, any sort `α`, any function `β : α → Sort u_3`, and any instance `i` of `DFunLike F α β`, the function that sends `f` to its coercion to a function `⇑f` is injective. In other words, if the function-application results of two different instances of `DFunLike F α β` are the same for all inputs, then the two instances are the same. This theorem guarantees that we cannot have two distinct `DFunLike` instances that behave identically when used as functions.
More concisely: If two functions `β : α -> Sort u_3` have the same coercions to functions for all `f : α` under the same `DFunLike F α β` instance, then those instances are equal.
|
DFunLike.coe_fn_eq
theorem DFunLike.coe_fn_eq :
∀ {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] {f g : F}, ⇑f = ⇑g ↔ f = g
This theorem states that for any dependent function-like object `F` (of sort `u_1`), that takes an input of sort `α` (of sort `u_2`) and maps to sort `β` (of sort `u_3`), given the instance `i` of dependent function-like behaviour for `F`, `α` and `β`, then for any two objects `f` and `g` of type `F`, if the function application of `f` is the same as the function application of `g` (denoted as `⇑f = ⇑g`), then `f` itself is equal to `g` and vice-versa. Essentially, it is stating that if two dependent function-like objects have the same effect when applied, they must be the same object.
More concisely: Given a dependent function-like object `F` from sort `α` to sort `β`, if two elements `f` and `g` of `F` have the same application, i.e., `⇑f = ⇑g`, then `f` and `g` are equal.
|