atomic — Mathlib

English

Embedding of an ordered finpartition into a sigma-type is defined by length, part sizes, and embedding map.

Русский

Встраивание упорядоченного конечного разделения в сигма-тип задано длиной, размерами частей и вложенной отображением.

LaTeX

$$$\lambda c. ⟨⟨c.length, (Order.lt\_add\_one_iff.2 c.length\le\)⟩, \dots⟩$$$

Lean4

/-- The ordered finpartition of `Fin n` into singletons. -/
@[simps -fullyApplied]
def atomic (n : ℕ) : OrderedFinpartition n where
  length := n
  partSize _ := 1
  partSize_pos _ := _root_.zero_lt_one
  emb m _ := m
  emb_strictMono _ := Subsingleton.strictMono _
  parts_strictMono := strictMono_id
  disjoint _ _ _ _ h := by simpa using h
  cover m := by simp

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