IsNatEquiv — Mathlib

English

The predicate IsNatEquiv defines a naturality condition for a family of equivalences between F_j and piLT X j.

Русский

IsNatEquiv задаёт натуральность семейства эквивалентностей между F_j и piLT X j.

LaTeX

$$$\\mathrm{IsNatEquiv}\\; (equiv) : \\forall (j,k) (hj hk) (h) (x), equiv(k, f h x) = piLTProj(h, equiv(j, x))$$$

Lean4

/-- The predicate that says a family of equivalences between `F j` and `piLT X j`
  is a natural transformation. -/
def IsNatEquiv {s : Set ι} (equiv : ∀ j : s, F j ≃ piLT X j) : Prop :=
  ∀ ⦃j k⦄ (hj : j ∈ s) (hk : k ∈ s) (h : k ≤ j) (x : F j), equiv ⟨k, hk⟩ (f h x) = piLTProj h (equiv ⟨j, hj⟩ x)

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