mk_eq_top_iff — Mathlib

English

For p ⊤ and any x with hx, the subtype element ⟨x, hx⟩ equals ⊤ in the subtype if and only if x = ⊤ in α.

Русский

Для p ⊤ и любого x с hx, элемент подтипа ⟨x, hx⟩ равен ⊤ в подтипе тогда и только тогда, когда x = ⊤ в α.

LaTeX

$$$\text{mk} \; x\; hx = \top \iff x = \top$$$

Lean4

@[simp]
theorem mk_eq_top_iff [OrderTop α] [OrderTop (Subtype p)] (htop : p ⊤) {x : α} (hx : p x) :
    (⟨x, hx⟩ : Subtype p) = ⊤ ↔ x = ⊤ :=
  (coe_eq_top_iff htop).symm

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