Theorems · Theorem · combinatorics

Fintype.card_subtype_or_disjoint

∀ {α : Type u_1} (p q : α → Prop),
  Disjoint p q →
    ∀ [inst : Fintype { x // p x }] [inst_1 : Fintype { x // q x }] [inst_2 : Fintype { x // p x ∨ q x }],
      Fintype.card { x // p x ∨ q x } = Fintype.card { x // p x } + Fintype.card { x // q x }

Defined in

Mathlib.Data.Fintype.Sum

Cited by

2 results in Mathlib

Foundations

Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeFintypeFintype