instPartialOrder — Mathlib

English

The partial order on Finpartition(a) is defined by the refinement relation; if P ≤ Q and Q ≤ R then P ≤ R, antisymmetry holds, etc.

Русский

У Finpartition(a) имеется частичный порядок по отношению к упорядочению: P ≤ Q и Q ≤ R следует, что P ≤ R; выполняется антисимметрия и т. д.

LaTeX

$$$\text{PartialOrder}(\mathrm{Finpartition}(a))$ with le as above; le_refl, le_trans, le_antisymm$$

Lean4

instance : PartialOrder (Finpartition a) :=
  {
    (inferInstance : LE (Finpartition
          a)) with
    le_refl := fun _ b hb ↦ ⟨b, hb, le_rfl⟩
    le_trans := fun _ Q R hPQ hQR b hb ↦ by
      obtain ⟨c, hc, hbc⟩ := hPQ hb
      obtain ⟨d, hd, hcd⟩ := hQR hc
      exact ⟨d, hd, hbc.trans hcd⟩
    le_antisymm := fun P Q hPQ hQP ↦ by
      ext b
      refine ⟨fun hb ↦ ?_, fun hb ↦ ?_⟩
      · obtain ⟨c, hc, hbc⟩ := hPQ hb
        obtain ⟨d, hd, hcd⟩ := hQP hc
        rwa [hbc.antisymm]
        rwa [P.disjoint.eq_of_le hb hd (P.ne_bot hb) (hbc.trans hcd)]
      · obtain ⟨c, hc, hbc⟩ := hQP hb
        obtain ⟨d, hd, hcd⟩ := hPQ hc
        rwa [hbc.antisymm]
        rwa [Q.disjoint.eq_of_le hb hd (Q.ne_bot hb) (hbc.trans hcd)] }

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