regionBetween — Mathlib

English

Definition: regionBetween(f,g,s) = { (x,t) : x ∈ s ∧ t ∈ Ioo(f x)(g x) }.

Русский

Определение: regionBetween(f,g,s) = { (x,t) : x ∈ s ∧ t ∈ Ioo(f(x))(g(x)) }.

LaTeX

$$$$ \\text{regionBetween}(f,g,s) = \\{ (x,t) : x \\in s \\wedge t \\in Ioo(f(x),g(x)) \\}. $$$$

Lean4

/-- The region between two real-valued functions on an arbitrary set. -/
def regionBetween (f g : α → ℝ) (s : Set α) : Set (α × ℝ) :=
  {p : α × ℝ | p.1 ∈ s ∧ p.2 ∈ Ioo (f p.1) (g p.1)}

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