Theorems · Theorem · logic and foundations

Relation.cutExpand_fibration

∀ {α : Type u_1} (r : α → α → Prop),
  Relation.Fibration (Prod.GameAdd (Relation.CutExpand r) (Relation.CutExpand r)) (Relation.CutExpand r) fun s =>
    s.1 + s.2

For any relation r on α, multiset addition Multiset α × Multiset α → Multiset α is a fibration between the game sum of CutExpand r with itself and CutExpand r itself.

Defined in

Mathlib.Logic.Hydra

Cited by

1 results in Mathlib

Foundations

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