index_out — Mathlib

English

The index of Quotient.out x equals the index of hs.out x, i.e., hs.index (Quotient.out x) = hs.index (hs.out x).

Русский

Индекс Quotient.out x равен индексу hs.out x, то есть hs.index (Quotient.out x) = hs.index (hs.out x).

LaTeX

$$$ hs.index (Quotient.out x) = hs.index (hs.out x) $$$

Lean4

/-- The indices of `Quotient.out` and `IndexedPartition.out` are equal. -/
theorem index_out (x : hs.Quotient) : hs.index x.out = hs.index (hs.out x) :=
  Quotient.inductionOn' x fun x => (Setoid.ker_apply_mk_out x).trans (hs.index_some _).symm

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