regionBetween_subset — Mathlib

English

RegionBetween(f,g,s) ⊆ s × univ, i.e., a region lies above s in the first coordinate and arbitrary second coordinate.

Русский

RegionBetween(f,g,s) ⊆ s × univ, то есть область лежит над s по первой координате и по второй произвольна.

LaTeX

$$$$ \\mathrm{regionBetween}(f,g,s) \\subseteq s \\times \\mathrm{univ}. $$$$

Lean4

theorem regionBetween_subset (f g : α → ℝ) (s : Set α) : regionBetween f g s ⊆ s ×ˢ univ := by
  simpa only [prod_univ, regionBetween, Set.preimage, setOf_subset_setOf] using fun a => And.left

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