apply_eq_bot_iff — Mathlib

English

Let f: α → β be strictly monotone with a bottom element ⊥ in the domain. Then f a = f ⊥ iff a = ⊥.

Русский

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

LaTeX

$$$f(a) = f(b) \\iff a = b$ при условии строго монотонности и наличия нижней границы; в частности $f(a) = f(\\bot) \\iff a = \\bot$.$$

Lean4

theorem apply_eq_bot_iff (hf : StrictMono f) : f a = f ⊥ ↔ a = ⊥ :=
  hf.dual.apply_eq_top_iff

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