OAI/SetTheory/PartitionPrinciple/Definability/CodedTemplateShadowLaws.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.CodedTemplateAttachment.old_lower_iff line 13
2. theorem OAI.PartitionPilot.Forcing.CodedTemplateAttachment.old_upper_iff line 18
3. theorem OAI.PartitionPilot.Forcing.CodedTemplateAttachment.cross_lower_iff line 22
4. theorem OAI.PartitionPilot.Forcing.CodedTemplateAttachment.encoded_shadow_meet line 27
5. theorem OAI.PartitionPilot.Forcing.CodedTemplateAttachment.encoded_cross_meet line 36
6. theorem OAI.PartitionPilot.Forcing.CodedTemplateAttachment.greatest_preserved line 48
7. theorem OAI.PartitionPilot.Forcing.CodedTemplateAttachment.least_preserved line 56