coe_eq_top_iff — Mathlib

English

For x in the subtype, x.val = ⊤ in α if and only if x = ⊤ in the subtype.

Русский

Для x в подтипе: x.val = ⊤ в α тогда и только тогда, когда x = ⊤ в подтипе.

LaTeX

$$$(x : {x // p x}) = \top^{\alpha} \iff x = \top^{Subtype p}$$$

Lean4

@[simp]
theorem coe_eq_top_iff [OrderTop α] [OrderTop (Subtype p)] (htop : p ⊤) {x : { x // p x }} : (x : α) = ⊤ ↔ x = ⊤ := by
  rw [← coe_top htop, Subtype.ext_iff]

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