W_iff_isLocallyBijective — Mathlib

English

Equivalence between W f and locally bijective predicate for f.

Русский

Эквивалентность между W f и локально биективным предикатом для f.

LaTeX

$$$J.W f \iff \big(\mathrm{Presheaf.IsLocallyInjective} J f \land \mathrm{Presheaf.IsLocallySurjective} J f\big).$$$

Lean4

theorem W_iff_isLocallyBijective : J.W f ↔ Presheaf.IsLocallyInjective J f ∧ Presheaf.IsLocallySurjective J f := by
  apply WEqualsLocallyBijective.iff

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