bind — Mathlib

English

The partial order on Finpartition(a) is defined via refinement; antisymmetry and transitivity hold with respect to ≤.

Русский

Частичный порядок на Finpartition(a) задаётся через упорядочение по уточнению; сохраняются транзитивность и антисимметрия.

LaTeX

$$$\text{PartialOrder}(\mathrm{Finpartition}(a))$ with le from refinement$$

Lean4

/-- Given a finpartition `P` of `a` and finpartitions of each part of `P`, this yields the
finpartition of `a` obtained by juxtaposing all the subpartitions. -/
@[simps]
def bind (P : Finpartition a) (Q : ∀ i ∈ P.parts, Finpartition i) : Finpartition a
    where
  parts := P.parts.attach.biUnion fun i ↦ (Q i.1 i.2).parts
  supIndep := by
    rw [supIndep_iff_pairwiseDisjoint]
    rintro a ha b hb h
    rw [Finset.mem_coe, Finset.mem_biUnion] at ha hb
    obtain ⟨⟨A, hA⟩, -, ha⟩ := ha
    obtain ⟨⟨B, hB⟩, -, hb⟩ := hb
    obtain rfl | hAB := eq_or_ne A B
    · exact (Q A hA).disjoint ha hb h
    · exact (P.disjoint hA hB hAB).mono ((Q A hA).le ha) ((Q B hB).le hb)
  sup_parts := by
    simp_rw [sup_biUnion]
    trans (sup P.parts id)
    · rw [eq_comm, ← Finset.sup_attach]
      exact sup_congr rfl fun b _hb ↦ (Q b.1 b.2).sup_parts.symm
    · exact P.sup_parts
  bot_notMem
    h := by
    rw [Finset.mem_biUnion] at h
    obtain ⟨⟨A, hA⟩, -, h⟩ := h
    exact (Q A hA).bot_notMem h

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