OAI/Analysis/SeparableQuotients/Positive/TransfiniteFamily.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SeparableQuotient.Positive.Family.continuum_large_density_family line 21
2. lemma OAI.SeparableQuotient.Positive.Family.real_dual_cardinal_le line 104
3. def OAI.SeparableQuotient.Positive.Family.evaluation line 121
4. lemma OAI.SeparableQuotient.Positive.Family.norm_evaluation_le line 124
5. theorem OAI.SeparableQuotient.Positive.Family.evaluation_family_of_density line 130