apply_eq_bot_iff

Mathlib.Order.BoundedOrder.Monotone

URI: https://scilib.ai/kg/mathlib#StrictAnti.apply_eq_bot_iff

English

Let f: α → β be strictly antitone with a bottom element ⊥. Then f a = f ⊥ iff a = ⊥.

Русский

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

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru