max_ne_top — Mathlib

English

Let α be a linear order with a top element ⊤. If a ≠ ⊤ and b ≠ ⊤, then max a b ≠ ⊤.

Русский

Пусть α — линейный порядок с верхней границей ⊤. Если a ≠ ⊤ и b ≠ ⊤, то max a b ≠ ⊤.

LaTeX

$$$a \\neq \\top \\to b \\neq \\top \\to \\max a b \\neq \\top$$$

Lean4

@[aesop (rule_sets := [finiteness]) safe apply]
theorem max_ne_top [OrderTop α] {a b : α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) : max a b ≠ ⊤ := by grind [max_eq_top]

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