OAI/Computability/DegreeRigidity/CohenForcing/ForcingSymmetry.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TuringRigidity.CountableForcing.Sentence.rename line 10
2. theorem OAI.TuringRigidity.CountableForcing.Sentence.forces_rename line 17
3. theorem OAI.TuringRigidity.CountableForcing.Sentence.weak_rename line 34
4. theorem OAI.TuringRigidity.CountableForcing.Sentence.weak_iff_dense_below line 38
5. theorem OAI.TuringRigidity.CountableForcing.Sentence.forces_weak line 49
6. theorem OAI.TuringRigidity.CountableForcing.Sentence.weak_incompatible line 53
7. def OAI.TuringRigidity.CountableForcing.Sentence.liftFirst line 60
8. theorem OAI.TuringRigidity.CountableForcing.Sentence.forces_liftFirst line 67
9. theorem OAI.TuringRigidity.CountableForcing.Sentence.weak_liftFirst line 81
10. theorem OAI.TuringRigidity.CountableForcing.Sentence.remove_tail_of_transport line 85