OAI/Analysis/PureInfiniteness/RelativeSupportAction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Relations on a positive support element extend to positive elements below it. This is the finite support calculation needed to combine abelian-range maps in the norm ultrapower.

  1. lemma OAI.WeakPureInfiniteness.mul_eq_zero_of_positive_le line 15
  2. lemma OAI.WeakPureInfiniteness.mul_eq_self_of_positive_le line 34