mem_lowerBounds_image — Mathlib

English

If f is monotone on t, s ⊆ t, a ∈ lowerBounds s, and a ∈ t, then f(a) ∈ lowerBounds (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{lowerBounds}(s)) \land (Hat : a \in t) \Rightarrow f(a) \in \mathrm{lowerBounds}(\mathrm{image}(f,s))$$$

Lean4

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

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