exists_inverse — Mathlib

English

For every c in OrderedFinpartition(n) and every j in Fin(n), there exists p = (m, r) in the disjoint union such that c.emb m r = j.

Русский

Для каждого c в OrderedFinpartition(n) и для каждого j в Fin(n) существует p = (m, r) из дизъюнктного объединения, такое что c.emb m r = j.

LaTeX

$$$\\exists p : \\Sigma m, \\mathrm{Fin}(c.partSize\\,m),\\; c.emb p.1\\,p.2 = j$$$

Lean4

theorem exists_inverse {n : ℕ} (c : OrderedFinpartition n) (j : Fin n) :
    ∃ p : Σ m, Fin (c.partSize m), c.emb p.1 p.2 = j :=
  by
  rcases c.cover j with ⟨m, r, hmr⟩
  exact ⟨⟨m, r⟩, hmr⟩

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