antisymmetrization_fibration — Mathlib

English

The relation LT on α and on its antisymmetrization forms a fibration with the quotient map to the antisymmetrization, i.e., lifting of LT respects the antisymmetrization.

Русский

Отношение LT на α и на его антисимметризацию образуют фибрацию относительно тождества по компоновке с фактор-множеством.

LaTeX

$$$\\text{Relation.Fibration}(\\lt, \\lt, \\text{toAntisymmetrization}(α, ≤))$$$

Lean4

theorem antisymmetrization_fibration : Relation.Fibration (· < ·) (· < ·) (toAntisymmetrization (α := α) (· ≤ ·)) :=
  by
  rintro a ⟨b⟩ h
  exact ⟨b, h, rfl⟩

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