restrictLe₂ — Mathlib

English

If a ≤ b, restrictLe₂ is the restriction to Iic b followed by restriction to Iic a.

Русский

Если a ≤ b, то restrictLe₂ — это ограничение до Iic b, затем ограничение до Iic a.

LaTeX

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

Lean4

/-- If a function `f` indexed by `α` is restricted to elements `≤ π`, and `a ≤ b`,
this is the restriction to elements `≤ a`. -/
def restrictLe₂ {a b : α} (hab : a ≤ b) :=
  Set.restrict₂ (π := π) (Iic_subset_Iic.2 hab)

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