restrictLe₂_apply — Mathlib

English

Evaluating restricted2 at i uses the lifted index i with the corresponding inclusion.

Русский

При вычислении restrictLe₂ на i применяем индекс i со сводкой включения.

LaTeX

$$$\\forall {a b : \\alpha} (hab : a \\le b) (f : (i : Iic b) \\to \\pi i) (i : Iic a),\\; restrictLe_2 hab f i = f \\langle i.1, Iic\\_subset\\_Iic.2 hab i.2 \\rangle$$$

Lean4

@[simp]
theorem restrictLe₂_apply {a b : α} (hab : a ≤ b) (f : (i : Iic b) → π i) (i : Iic a) :
    restrictLe₂ hab f i = f ⟨i.1, Iic_subset_Iic.2 hab i.2⟩ :=
  rfl

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