ofDual_inj — Mathlib

English

Let α be a type. For all a,b ∈ αᵒᵈ, we have that ofDual a = ofDual b if and only if a = b.

Русский

Пусть α — множество. Для любых a, b ∈ αᵒᵈ верно: ofDual a = ofDual b тогда и только тогда, когда a = b.

LaTeX

$$$\forall a,b \in \alpha^{\mathrm{op}},\quad \operatorname{ofDual} a = \operatorname{ofDual} b \iff a=b$$$

Lean4

theorem ofDual_inj {a b : αᵒᵈ} : ofDual a = ofDual b ↔ a = b := by simp

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