Theorems · Theorem · combinatorics

Finset.bipartiteBelow.congr_simp

∀ {α : Type u_2} {β : Type u_3} (r r_1 : α → β → Prop),
  r = r_1 →
    ∀ (s s_1 : Finset α),
      s = s_1 →
        ∀ (b b_1 : β),
          b = b_1 →
            ∀ {inst : (a : α) → Decidable (r a b)} [inst_1 : (a : α) → Decidable (r_1 a b_1)],
              Finset.bipartiteBelow r s b = Finset.bipartiteBelow r_1 s_1 b_1

Defined in

Mathlib.Combinatorics.Enumerative.DoubleCounting

Cited by

2 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext, Quot.sound

Assumes

Decidable