le_apply_iff — Mathlib

English

Characterization of when b ≤ f(a) holds: equivalence with an element mapping to b below a.

Русский

Характеризация условия b ≤ f(a): эквивалентно существованию c ≤ a с f(c) = b.

LaTeX

$$b \le f(a) \iff \exists c \le a,\ f(c) = b$$

Lean4

theorem le_apply_iff [PartialOrder α] (f : α ≤i β) : b ≤ f a ↔ ∃ c ≤ a, f c = b :=
  by
  constructor
  · intro h
    obtain ⟨c, hc⟩ := f.mem_range_of_le h
    refine ⟨c, ?_, hc⟩
    rwa [← hc, f.le_iff_le] at h
  · rintro ⟨c, hc, rfl⟩
    exact f.monotone hc

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