card_mono — Mathlib

English

If P ≤ Q, then the cardinality of Q.parts is at most the cardinality of P.parts.

Русский

Если P ≤ Q, то |Q.parts| ≤ |P.parts|.

LaTeX

$$$P \le Q \Rightarrow |Q.\text{parts}| \le |P.\text{parts}|$$

Lean4

theorem card_mono {a : α} {P Q : Finpartition a} (h : P ≤ Q) : #Q.parts ≤ #P.parts := by
  classical
  have : ∀ b ∈ Q.parts, ∃ c ∈ P.parts, c ≤ b := fun b ↦ exists_le_of_le h
  choose f hP hf using this
  rw [← card_attach]
  refine card_le_card_of_injOn (fun b ↦ f _ b.2) (fun b _ ↦ hP _ b.2) fun b _ c _ h ↦ ?_
  exact
    Subtype.coe_injective
      (Q.disjoint.elim b.2 c.2 fun H ↦
        P.ne_bot (hP _ b.2) <| disjoint_self.1 <| H.mono (hf _ b.2) <| h.le.trans <| hf _ c.2)

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