OAI/SetTheory/PartitionPrinciple/Forcing/MeetOrderPosetActions.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.MeetOrder.toPartialOrder line 12
2. def OAI.PartitionPilot.Compression.MeetIso.toOrderIso line 24
3. def OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.toPosetAction line 45
4. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.principalFix_eq line 51
5. theorem OAI.PartitionPilot.Compression.RecursiveMaps.CosetGeometry.OrderAction.actionGraph_eq line 55
6. theorem OAI.PartitionPilot.SetRealization.GeometryPresentation.conditionOrder_eq line 65