mk_coe — Mathlib

English

If we form a model with corners from a partial equivalence e and additional data, the resulting model's underlying map to E is exactly e.

Русский

Если построить модель с углами из частичного эквивалента e и дополнительных данных, полученная модель имеет в качестве отображения в E именно e.

LaTeX

$$$ \\bigl( \\mathrm{ModelWithCorners.mk}\\, e\, a\, b\, c\, d\, d' \\bigr) : H \\to E = e $$$

Lean4

@[simp, mfld_simps]
theorem mk_coe (e : PartialEquiv H E) (a b c d d') :
    ((ModelWithCorners.mk e a b c d d' : ModelWithCorners 𝕜 E H) : H → E) = (e : H → E) :=
  rfl

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