English
Binary pushforward of nonempty intervals: given a function f: α × β → γ and monotonicity hypotheses h₀, h₁, there is a well-defined operation map₂ that sends a ∈ NonemptyInterval α and b ∈ NonemptyInterval β to the interval in γ with endpoints (f(a.fst, b.fst), f(a.snd, b.snd)).
Русский
Двоичное отображение границ ненулевых интервалов: задана функция f: α×β→γ и предположения монотонности; определяется отображение map₂, которое отправляет (a,b) ∈ NonemptyInterval α × NonemptyInterval β в интервальный элемент γ с пределами (f(a.fst,b.fst), f(a.snd,b.snd)).
LaTeX
$$$\text{map}_2(f,h_0,h_1)(s,t) = \langle (f(s.fst,t.fst), f(s.snd,t.snd)), \dots \rangle$$$
Lean4
/-- Binary pushforward of nonempty intervals. -/
@[simps]
def map₂ (f : α → β → γ) (h₀ : ∀ b, Monotone fun a => f a b) (h₁ : ∀ a, Monotone (f a)) :
NonemptyInterval α → NonemptyInterval β → NonemptyInterval γ := fun s t =>
⟨(f s.fst t.fst, f s.snd t.snd), (h₀ _ s.fst_le_snd).trans <| h₁ _ t.fst_le_snd⟩
