image2_lowerBounds_upperBounds_subset_upperBounds_image2

English

If f is antitone in the first argument and monotone in the second, then image2 f (lowerBounds s) (upperBounds t) is contained in upperBounds (image2 f s t).

Русский

Если f антимонотонна по первому аргументу и монотонна по второму, то image2 f (lowerBounds s) (upperBounds t) ⊆ upperBounds (image2 f s t).

LaTeX

$$ (∀ (b), Antitone (swap f b)) → (∀ a, Monotone (f a)) → image2 f (lowerBounds s) (upperBounds t) ⊆ upperBounds (image2 f s t)$$

Lean4

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

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