OAI/Analysis/StrictMeans/FiberSum.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.StrictInverseFirstPower.fiberSum line 11
2. lemma OAI.StrictInverseFirstPower.fiberSum_le_of_injection line 14
3. lemma OAI.StrictInverseFirstPower.fiberSum_iUnion line 30
4. lemma OAI.StrictInverseFirstPower.fiberSum_eq_single line 43
5. lemma OAI.StrictInverseFirstPower.fiberSum_eq_zero_of_not_mem_image line 50
6. lemma OAI.StrictInverseFirstPower.fiberSum_eq_indicator_inverse line 55