optionCongr_eq_equivFunctor_mapEquiv

English

When α and β live in the same universe, optionCongr e coincides with EquivFunctor.mapEquiv Option e.

Русский

Если области определения совпадают по вселенной, то optionCongr e равняется EquivFunctor.mapEquiv Option e.

LaTeX

$$$\\text{optionCongr } e = \\text{EquivFunctor.mapEquiv } \\text{Option } e$.$$

Lean4

/-- When `α` and `β` are in the same universe, this is the same as the result of
`EquivFunctor.mapEquiv`. -/
theorem optionCongr_eq_equivFunctor_mapEquiv {α β : Type u} (e : α ≃ β) :
    optionCongr e = EquivFunctor.mapEquiv Option e :=
  rfl

Похожие утверждения