Equiv.optionCongr_eq_equivFunctor_mapEquiv
theorem Equiv.optionCongr_eq_equivFunctor_mapEquiv :
∀ {α β : Type u} (e : α ≃ β), e.optionCongr = EquivFunctor.mapEquiv Option e
The theorem `Equiv.optionCongr_eq_equivFunctor_mapEquiv` states that for any two types `α` and `β` in the same universe `u`, given an equivalence `e` between `α` and `β`, the equivalence induced by `e` on their option types is the same as the result of applying the `EquivFunctor.mapEquiv` operation to `Option` with `e`. This essentially asserts that `EquivFunctor.mapEquiv` behaves as expected when applied to option types.
More concisely: For any equivalence `e` between types `α` and `β` in the same universe `u`, the equivalence between their option types induced by `e` is equal to `EquivFunctor.mapEquiv Option e`.
|
Equiv.optionCongr_refl
theorem Equiv.optionCongr_refl : ∀ {α : Type u_1}, (Equiv.refl α).optionCongr = Equiv.refl (Option α)
The theorem `Equiv.optionCongr_refl` states that for any type `α`, the application of the `Equiv.optionCongr` function (which maps an equivalence between types `α` and `β` to an equivalence between `Option α` and `Option β`) to the identity equivalence `Equiv.refl α` (which is an equivalence between a type `α` and itself) is equivalent to the identity equivalence `Equiv.refl (Option α)` (which is an equivalence between `Option α` and itself). In other words, this theorem is saying that mapping a type to the corresponding option type, when the original map is the identity map, results in the identity map on the option types.
More concisely: The theorem `Equiv.optionCongr_refl` asserts that the application of `Equiv.optionCongr` to the identity equivalence on type `α` results in the identity equivalence on `Option α`.
|
Equiv.removeNone_some
theorem Equiv.removeNone_some :
∀ {α : Type u_1} {β : Type u_2} (e : Option α ≃ Option β) {x : α},
(∃ x', e (some x) = some x') → some (e.removeNone x) = e (some x)
This theorem, `Equiv.removeNone_some`, states that for any two types `α` and `β`, given an equivalence `e` between the `Option` types of `α` and `β`, and for any element `x` of type `α`, if there exists an `x'` such that applying the equivalence `e` to `some x` results in `some x'`, then applying the function `some` to the result of `Equiv.removeNone e` of `x` is equivalent to applying `e` to `some x`. In other words, the equation `some ((Equiv.removeNone e) x) = e (some x)` holds under the given conditions. This theorem essentially shows that we can safely remove `none` from the equivalence between the `Option` types without changing the results for elements that are not `none`.
More concisely: For any equivalence between `Option` types `e` and any `x` in type `α`, if `e (some x) = some y` for some `y`, then `some (Equiv.removeNone e x) ≡ e (some x)`.
|