ne_top_iff_eq — Mathlib

English

Let a be a coatom and a ≤ b. Then b is not the top if and only if b = a.

Русский

Пусть a — коатом и a ≤ b. Тогда b не равно верхнему элементу ⊤ тогда и только тогда, когда b = a.

LaTeX

$$$ \\mathrm{IsCoatom}(a) \\wedge (a \\le b) \\rightarrow (b \\neq \\top \\leftrightarrow b = a).$$$

Lean4

theorem ne_top_iff_eq (ha : IsCoatom a) (hab : a ≤ b) : b ≠ ⊤ ↔ b = a :=
  (ha.ne_iff_eq_top hab).not_right.symm

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