sections_ext_iff — Mathlib

English

Two sections x,y of F are equal if and only if their components are equal at every j: x = y iff ∀ j, x.val j = y.val j.

Русский

Две секции x,y функторa F равны тогда и только тогда, когда их компоненты равны для каждого j: x = y ⇔ ∀ j, x.val j = y.val j.

LaTeX

$$$$ x = y \iff \forall j,\ x.\text{val}(j) = y.\text{val}(j). $$$$

Lean4

theorem sections_ext_iff {F : J ⥤ Type w} {x y : F.sections} : x = y ↔ ∀ j, x.val j = y.val j :=
  Subtype.ext_iff.trans funext_iff

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