mk_eq_zero — Mathlib

English

For any hx: 0 ≤ x, the element ⟨x, hx⟩ equals 0 in the nonnegative subtype iff x = 0.

Русский

Для любого hx: 0 ≤ x элемент ⟨x, hx⟩ равен 0 в подпредмете тогда и только тогда, когда x = 0.

LaTeX

$$$mk\_eq\_zero : \\forall x, 0 ≤ x \\Rightarrow (⟨x, hx⟩ = 0) \\iff x = 0$$$

Lean4

@[simp]
theorem mk_eq_zero [Zero α] [Preorder α] {x : α} (hx : 0 ≤ x) : (⟨x, hx⟩ : { x : α // 0 ≤ x }) = 0 ↔ x = 0 :=
  Subtype.ext_iff

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