frestrictLe₂ — Mathlib

English

Frestricted Le with two bounds is the restriction to a ≤ b, seen as a finite restriction.

Русский

FrestrictLe₂ с двумя границами — это ограничение до a ≤ b, рассматриваемое как конечное ограничение.

LaTeX

$$$\\text{frestrictLe}_2(a,b) := \\text{restrict}_2(\\pi := \\pi) (Iic\\_subset\\_Iic.2 hab)$$$

Lean4

/-- If a function `f` indexed by `α` is restricted to elements `≤ b`, and `a ≤ b`,
this is the restriction to elements `≤ b`. Intervals are seen as finite sets. -/
def frestrictLe₂ {a b : α} (hab : a ≤ b) :=
  restrict₂ (π := π) (Iic_subset_Iic.2 hab)

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