mem_upperBounds_image2_of_mem_lowerBounds

English

If s has a least element a and t has a greatest element b, then f(a,b) is least in image2 f s t.

Русский

Если в s есть наименьший элемент a и в t — наибольший b, то f(a,b) наименьшее в image2 f s t.

LaTeX

$$IsLeast s a \rightarrow IsGreatest t b \rightarrow IsLeast (image2 f s t) (f a b)$$

Lean4

theorem mem_upperBounds_image2_of_mem_lowerBounds (ha : a ∈ lowerBounds s) (hb : b ∈ lowerBounds t) :
    f a b ∈ upperBounds (image2 f s t) :=
  forall_mem_image2.2 fun _ hx _ hy => (h₀ _ <| ha hx).trans <| h₁ _ <| hb hy

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