overEquiv_symm_iff — Mathlib

English

For Sieve S on Y and morphism f: Z → Y, (overEquiv Y).symm S f holds iff S f.left holds.

Русский

Для севея S на Y и морфизма f: Z → Y, (overEquiv Y).symm S f выполняется тогда и только тогда, когда S f.left выполняется.

LaTeX

$$(overEquiv Y).symm S f ↔ S f.left$$

Lean4

@[simp]
theorem overEquiv_symm_iff {X : C} {Y : Over X} (S : Sieve Y.left) {Z : Over X} (f : Z ⟶ Y) :
    (overEquiv Y).symm S f ↔ S f.left := by rfl

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