Авторский контракт интерпретации порядка Arxo

ru · unofficial · sha256:b3d6a483d3fde836b357093f6f6eaab406950c1596d1f2769435e9079dd98b5e

Авторский контракт интерпретации порядков Arxo, версия 0.1.0. Order обозначает носитель с одним выбранным предпорядком. Element обозначает элемент; принадлежность конкретному носителю задаётся in_carrier. preorder_structure — явное предположение о выбранном предпорядке, а не результат проверки всех его аксиом. Отношения before_or_equal и strictly_before интерпретируются как нестрогое и строгое отношения выбранного порядка. При наличии guard порядка и принадлежности всех элементов применяются четыре положительных правила: строгая транзитивность; из x≤y и y<z следует x<z; из x<y следует x≤y; нестрогая транзитивность. partial_order_structure и linear_order_structure — явные предположения о выбранном частичном и линейном порядке на том же носителе. Иерархия структур задаётся двумя положительными правилами: частичный порядок даёт guard предпорядка, линейный порядок даёт guard частичного порядка. Обратного вывода нет. Правила используют положительную поддержку supported. Контракт не вводит замкнутость мира, не сравнивает произвольные числа и не проверяет эквивалентность определений Lean и Isabelle. Исходные теоремы и разрешения импорта находятся у отдельных владельцев mathlib.order и isabelle.order. Совместный сертификат принадлежит arxo.order_composition.

Ссылаются нормы: Element, LinearOrderIsPartialOrder, Order, PartialOrderIsPreorder, StrictImpliesWeak, StrictTransitivity, WeakThenStrict, WeakTransitivity, before_or_equal, in_carrier, linear_order_structure, partial_order_structure, preorder_structure, strictly_before