mpullback_eq_pullback — Mathlib

English

Equality mpullbackWithin_eq_pullbackWithin: for f, V, s, mpullbackWithin I I' f V s = pullbackWithin 𝕜 f V s.

Русский

Эквивалентность mpullbackWithin eq pullbackWithin: mpullbackWithin I I' f V s = pullbackWithin 𝕜 f V s.

LaTeX

$$$$ \mathrm{mpullbackWithin}\ I\ I' f V s = \mathrm{pullbackWithin}\ 𝕜 f V s $$$$

Lean4

theorem mpullback_eq_pullback {f : E → E'} {V : E' → E'} : mpullback 𝓘(𝕜, E) 𝓘(𝕜, E') f V = pullback 𝕜 f V := by
  simp only [← mpullbackWithin_univ, ← pullbackWithin_univ, mpullbackWithin_eq_pullbackWithin]

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