hasSeparator_op_iff — Mathlib

English

HasSeparator (Cᵒᵖ) ↔ HasCoseparator C.

Русский

Имеется разделитель в Opposite C эквивалентно наличию косепаратора в C.

LaTeX

$$$\mathrm{HasSeparator}(C^{\mathrm{op}}) \iff \mathrm{HasCoseparator}(C)$$

Lean4

@[simp]
theorem hasSeparator_op_iff : HasSeparator Cᵒᵖ ↔ HasCoseparator C :=
  ⟨fun ⟨G, hG⟩ => ⟨unop G, (isCoseparator_unop_iff G).mpr hG⟩, fun ⟨G, hG⟩ => ⟨op G, (isSeparator_op_iff G).mpr hG⟩⟩

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