parts_inf — Mathlib

English

The infimum of P and Q has parts equal to the image of the pairwise infimum of their parts, erased with ⊥.

Русский

Перемножение инфимумов дает разбиение, чьи блоки соответствуют образу пары блоков, взятых через inf.

LaTeX

$$$(P \sqcap Q).parts = ((P.parts \times\! Q.parts).image (\lambda bc. bc.1 \land bc.2)).erase(\bot)$$$

Lean4

@[simp]
theorem parts_inf (P Q : Finpartition a) :
    (P ⊓ Q).parts = ((P.parts ×ˢ Q.parts).image fun bc : α × α ↦ bc.1 ⊓ bc.2).erase ⊥ :=
  rfl

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