le_prevFixed_iff

Mathlib.Order.FixedPoints

URI: https://scilib.ai/kg/mathlib#OrderHom.le_prevFixed_iff

English

For x with f(x) ≤ x, y ≤ prevFixed(x) iff y ≤ x (in fixed points).

Русский

При x с f(x) ≤ x, y ≤ prevFixed(x) тогда и только тогда y ≤ x.

LaTeX

$$$f(x) \le x \Rightarrow (y \le f.prevFixed(x) \Leftrightarrow y \le x).$$$

Lean4

@[simp]
theorem le_prevFixed_iff {x : α} (hx : f x ≤ x) {y : fixedPoints f} : y ≤ f.prevFixed x hx ↔ ↑y ≤ x :=
  f.dual.nextFixed_le_iff hx

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

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

Разделы

Аффилиация

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