opEquiv_self — Mathlib

English

The members of the opposite of a set are in bijection with the members of the set itself.

Русский

Элементы множества в противоположном типе лежат в биекции с элементами самого множества.

LaTeX

$$s.op ≃ s$$

Lean4

/-- The members of the opposite of a set are in bijection with the members of the set itself. -/
@[simps]
def opEquiv_self (s : Set α) : s.op ≃ s :=
  ⟨fun x ↦ ⟨unop x, x.2⟩, fun x ↦ ⟨op x, x.2⟩, fun _ ↦ rfl, fun _ ↦ rfl⟩

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