theorem
proved
preorder_refl
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RecogGeom.Comparative on GitHub at line 85.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
82 notGreaterThan R gt_events c₁ c₃
83
84/-- When a comparative recognizer induces a preorder, we get reflexivity for free -/
85theorem preorder_refl (R : ComparativeRecognizer C E) (gt_events : Set E)
86 (h : InducesPreorder R gt_events) (c : C) :
87 notGreaterThan R gt_events c c := by
88 unfold notGreaterThan
89 rw [R.compare_self]
90 exact h.eq_not_gt
91
92/-- The induced preorder relation -/
93def inducedPreorder (R : ComparativeRecognizer C E) (gt_events : Set E)
94 (h : InducesPreorder R gt_events) : Preorder C where
95 le := notGreaterThan R gt_events
96 le_refl := preorder_refl R gt_events h
97 le_trans := fun _ _ _ => h.trans _ _ _
98
99/-! ## Recognition Partial Order -/
100
101/-- A comparative recognizer induces a partial order when it's also antisymmetric:
102 c₁ ≤ c₂ and c₂ ≤ c₁ implies c₁ = c₂ -/
103structure InducesPartialOrder (R : ComparativeRecognizer C E) (gt_events : Set E)
104 extends InducesPreorder R gt_events : Prop where
105 /-- Antisymmetry -/
106 antisymm : ∀ c₁ c₂, notGreaterThan R gt_events c₁ c₂ →
107 notGreaterThan R gt_events c₂ c₁ → c₁ = c₂
108
109/-- The induced partial order relation -/
110def inducedPartialOrder (R : ComparativeRecognizer C E) (gt_events : Set E)
111 (h : InducesPartialOrder R gt_events) : PartialOrder C where
112 le := notGreaterThan R gt_events
113 le_refl := preorder_refl R gt_events h.toInducesPreorder
114 le_trans := fun _ _ _ => h.trans _ _ _
115 le_antisymm := fun _ _ => h.antisymm _ _