WithZero.coe_inj
theorem WithZero.coe_inj : ∀ {α : Type u} {a b : α}, ↑a = ↑b ↔ a = b
This theorem, `WithZero.coe_inj`, states that for any given type `α` and any two elements `a` and `b` of that type, the statement that the coersion of `a` to `WithZero α` is equal to the coersion of `b` to `WithZero α` is equivalent to the statement that `a` is equal to `b`. In other words, the coersion to `WithZero α` is an injective (or one-to-one) function.
More concisely: The coersion function from a type to `WithZero` is an injection.
|
WithZero.coe_ne_zero
theorem WithZero.coe_ne_zero : ∀ {α : Type u} {a : α}, ↑a ≠ 0
This theorem, `WithZero.coe_ne_zero`, states that for all types `α` and for all elements `a` of type `α`, the coercion of `a` to `WithZero α` is not equal to zero. In other words, no non-zero value from an arbitrary type `α` can become zero when lifted into the `WithZero α` type via coercion.
More concisely: For all types `α` and elements `a` of type `α`, the coercion of `a` to `WithZero α` is never equal to the zero element of `WithZero α`.
|
WithOne.cases_on
theorem WithOne.cases_on : ∀ {α : Type u} {P : WithOne α → Prop} (x : WithOne α), P 1 → (∀ (a : α), P ↑a) → P x := by
sorry
This theorem, `WithOne.cases_on`, is a case analysis principle for an extended type `WithOne α`. Given an arbitrary type `α`, the function `WithOne` adds a new element `1` to the type `α`. This theorem states that for any property `P` that might hold over the elements of the type `WithOne α`, and for any element `x` of `WithOne α`, if `P` holds for `1` and `P` also holds for any element of `α` (when considered as an element of `WithOne α`), then `P` must hold for `x`. This theorem is essentially a way to perform case analysis over the members of the type `WithOne α`, separating the 'extra' element `1` and the 'original' elements from `α`.
More concisely: For any property `P` and element `x` of `WithOne α`, if `P` holds for `1` in `WithOne α` and `P` holds for all elements of `α` considered as elements of `WithOne α`, then `P` holds for `x`.
|
WithZero.cases_on
theorem WithZero.cases_on : ∀ {α : Type u} {P : WithZero α → Prop} (x : WithZero α), P 0 → (∀ (a : α), P ↑a) → P x := by
sorry
This theorem states that given any type `α`, and a property `P` that applies to elements of the type `WithZero α`, for any element `x` of `WithZero α`, if we can prove that the property `P` holds for `0` and for all the elements in `α` (note that elements in `α` are also in `WithZero α`), then we can conclude that the property `P` holds for `x`.
In other words, this theorem provides a method to prove that a property holds for all elements in `WithZero α`: we just need to prove it for `0` and for all elements in `α`.
More concisely: If `P` is a property that holds for `0` and all elements in `α` where `α` has a zero element, then `P` holds for every element `x` in `WithZero α` (the type of `α` with an added zero element).
|