image2_upperBounds_upperBounds_subset

English

For a strictly monotone function f, a is in the upper bounds of s iff f(a) is in the upper bounds of f[s].

Русский

Для строго монотонной функции f: a принадлежит верхним границам s тогда и только тогда, когда f(a) принадлежит верхним границам f[s].

LaTeX

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

Lean4

theorem image2_upperBounds_upperBounds_subset : image2 f (upperBounds s) (upperBounds t) ⊆ upperBounds (image2 f s t) :=
  image2_subset_iff.2 fun _ ha _ hb ↦ mem_upperBounds_image2 h₀ h₁ ha hb

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