mem_range_of_le — Mathlib

English

Let f be an initial-seg embedding of α into β. If b ≤ f(a) for some a ∈ α and b ∈ β, then b lies in the image of f; i.e., there exists a' ∈ α with f(a') = b.

Русский

Пусть f — вложение начального сегмента α в β. Если b ≤ f(a) для некоторого a ∈ α и b ∈ β, то b принадлежит образу f; т.е. существует a' ∈ α такое, что f(a') = b.

LaTeX

$$$\forall a \in \alpha, \forall b \in \beta:\ b \le f(a) \Rightarrow \exists a' \in \alpha,\ f(a') = b$$$

Lean4

theorem mem_range_of_le [LT α] (f : α ≤i β) (h : b ≤ f a) : b ∈ Set.range f :=
  by
  obtain rfl | hb := h.eq_or_lt
  exacts [⟨a, rfl⟩, f.mem_range_of_rel hb]

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