image2_upperBounds_lowerBounds_subset_lowerBounds_image2

English

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

Русский

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

LaTeX

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

Lean4

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

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