mem_upperBounds_image2 — Mathlib

English

An strictly antitone map sends a least element to a greatest element of its image.

Русский

Строго антитонная карта отправляет наименьший элемент в наибольший элемент образа.

LaTeX

$$IsLeast(s,a) \rightarrow IsGreatest(f''(s)) (f(a))$$

Lean4

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

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