mem_upperBounds_image — Mathlib

English

Let α, β be preordered, f: α → β monotone on t, s ⊆ t. If a is an upper bound of s and a ∈ t, then f(a) is an upper bound of the image f''s.

Русский

Пусть α, β упорядочены, f: α → β монотонна на t, s ⊆ t. Если a является верхней границей s и a ∈ t, то f(a) является верхней границей образа f''s.

LaTeX

$$$(Hf : MonotoneOn\ f\ t) \land (Hst : s \subseteq t) \land (Has : a \in \mathrm{upperBounds}(s)) \land (Hat : a \in t) \Rightarrow f(a) \in \mathrm{upperBounds}(\mathrm{image}(f,s))$$$

Lean4

theorem mem_upperBounds_image (Hf : MonotoneOn f t) (Hst : s ⊆ t) (Has : a ∈ upperBounds s) (Hat : a ∈ t) :
    f a ∈ upperBounds (f '' s) :=
  forall_mem_image.2 fun _ H => Hf (Hst H) Hat (Has H)

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