frestrictLe₂_apply — Mathlib

English

Evaluation rule for frestrictLe₂ on i, using i's underlying value and the subset.

Русский

Правило вычисления frestrictLe₂ на i через i.значение и подмножество.

LaTeX

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

Lean4

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

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