sectionsEquiv_apply_val — Mathlib

English

For s ∈ I.sections and i ∈ J.L, c.ι i (sectionsEquiv hc s) = s.val i.

Русский

Для s ∈ I.sections и i ∈ J.L, c.ι i (sectionsEquiv hc s) = s.val i.

LaTeX

$$$\\forall s:\\, I.sections\\;\\forall i:\\, J.L:\\; c.\\ι\\, i\\,(sectionsEquiv\\, hc\\, s) = s.\\text{val}\\, i$$$

Lean4

@[simp]
theorem sectionsEquiv_apply_val (s : I.sections) (i : J.L) : c.ι i (sectionsEquiv hc s) = s.val i :=
  by
  obtain ⟨x, rfl⟩ := (sectionsEquiv hc).symm.surjective s
  simp

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