lt_apply_iff — Mathlib

English

A similar criterion for strict inequality: b < f(a) iff there exists a' < a with f(a') = b.

Русский

Аналогично для строгого порядка: b < f(a) эквивалентно существованию a' < a, такого что f(a') = b.

LaTeX

$$b < f(a) \iff \exists a' < a,\ f(a') = b$$

Lean4

theorem lt_apply_iff [PartialOrder α] (f : α ≤i β) : b < f a ↔ ∃ a' < a, f a' = b :=
  by
  constructor
  · intro h
    obtain ⟨c, hc⟩ := f.mem_range_of_rel h
    refine ⟨c, ?_, hc⟩
    rwa [← hc, f.lt_iff_lt] at h
  · rintro ⟨c, hc, rfl⟩
    exact f.strictMono hc

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