objEquiv_symm_mem_nonDegenerate_iff_mono

English

For any f from the opposite of ⦋d⦌ to ⦋n⦌, the symmetry of objEquiv places f in Δ[n].nonDegenerate d iff f is mono.

Русский

Для любого f: ⦋d⦌ᵒ¹ ⟶ ⦋n⦌, симметрия objEquiv даёт, что f ∈ Δ[n].nonDegenerate d эквивалентно моно.

LaTeX

$$(objEquiv.{u} (m := (op ⦋d⦌))).symm f ∈ Δ[n].nonDegenerate d ↔ Mono f$$

Lean4

theorem objEquiv_symm_mem_nonDegenerate_iff_mono {n d : ℕ} (f : ⦋d⦌ ⟶ ⦋n⦌) :
    (objEquiv.{u} (m := (op ⦋d⦌))).symm f ∈ Δ[n].nonDegenerate d ↔ Mono f := by simp [mem_nonDegenerate_iff_mono]

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