apply_eq_top_iff — Mathlib

English

Let f: α → β be strictly monotone with α having a top element ⊤. Then f a = f ⊤ if and only if a = ⊤.

Русский

Пусть f: α → β строго монотонна и в источнике есть верхняя граница ⊤. Тогда f(a) = f(⊤) тогда и только тогда, когда a = ⊤.

LaTeX

$$$f(a) = f(\\top) \\iff a = \\top$$$

Lean4

theorem apply_eq_top_iff (hf : StrictMono f) : f a = f ⊤ ↔ a = ⊤ :=
  ⟨fun h => not_lt_top_iff.1 fun ha => (hf ha).ne h, congr_arg _⟩

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