image2_lowerBounds_lowerBounds_subset

English

For a strictly monotone f, f(a) is in the lower bounds of f'' s iff a is in the lower bounds of s.

Русский

Для строго монотонной f, f(a) принадлежит нижним границам образа ⇔ a принадлежит нижним границам s.

LaTeX

$$$ f a \in \mathrm{LB}(f''(s)) \iff a \in \mathrm{LB}(s) $$$

Lean4

theorem image2_lowerBounds_lowerBounds_subset : image2 f (lowerBounds s) (lowerBounds t) ⊆ lowerBounds (image2 f s t) :=
  image2_subset_iff.2 fun _ ha _ hb ↦ mem_lowerBounds_image2 h₀ h₁ ha hb

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