instLE — Mathlib

English

There is a refinement order on Finpartition(a): P ≤ Q iff every block of P is ≤ some block of Q.

Русский

Существует отношение упорядочения (≤) между Finpartition(a): P ≤ Q тогда, когда каждый блок P содержится внутри некоторого блока Q.

LaTeX

$$$\text{instance }\le:\ Finpartition(a) \to Finpartition(a)\to \mathrm{Prop}$ with $P \le Q$ defined by $\forall b\in P.parts, \exists c\in Q.parts, b \le c$$$

Lean4

/-- We say that `P ≤ Q` if `P` refines `Q`: each part of `P` is less than some part of `Q`. -/
instance : LE (Finpartition a) :=
  ⟨fun P Q ↦ ∀ ⦃b⦄, b ∈ P.parts → ∃ c ∈ Q.parts, b ≤ c⟩

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