OAI/Analysis/SymmetricDomains/NormalizedDisplacementZeroUniform.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Release061.iterateAverage_sub_id_bound_finite line 35
2. theorem OAI.Release061.Biholomorph.displacement_set_mem_nhds_one line 60
3. theorem OAI.Release061.Biholomorph.normalized_displacement_zero_of_uniform_small_powers line 70