opEquiv — Mathlib

English

There is a natural equivalence between Set α and Set αᵒᵖ given by taking opposites and unops.

Русский

Существует естественная эквивалентность между множествами над α и над αᵒᵖ, задаваемая отображением противоположностей и обратно.

LaTeX

$$Set α ≃ Set α^{\mathrm{op}}$$

Lean4

/-- Taking opposites as an equivalence of powersets. -/
@[simps]
def opEquiv : Set α ≃ Set αᵒᵖ :=
  ⟨Set.op, Set.unop, op_unop, unop_op⟩

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