Basic facts about cost factories.

ink

def Factory.lt {α : Type} (F : Factory α) (c₁ : α) (c₂ : α) : Prop

Equations

• Factory.lt F c₁ c₂ = (Factory.le F c₁ c₂ = true ∧ c₁ ≠ c₂)

ink

theorem Factory.le_refl {α : Type} {F : Factory α} (c : α) : Factory.le F c c = true

ink

theorem Factory.not_eq_of_not_le {α : Type} {F : Factory α} {c₁ : α} {c₂ : α} (h : ¬Factory.le F c₁ c₂ = true) : c₁ ≠ c₂

ink

theorem Factory.not_le_iff_lt {α : Type} {F : Factory α} {c₁ : α} {c₂ : α} : ¬Factory.le F c₁ c₂ = true ↔ Factory.lt F c₂ c₁

ink

theorem Factory.lt_trans {α : Type} {F : Factory α} {c₁ : α} {c₂ : α} {c₃ : α} (h₁ : Factory.lt F c₁ c₂) (h₂ : Factory.lt F c₂ c₃) : Factory.lt F c₁ c₃

ink

theorem Factory.le_of_lt {α : Type} {F : Factory α} {c : α} {c' : α} (h₁ : Factory.lt F c c') : Factory.le F c c' = true

ink

theorem Factory.invalid_inequality {α : Type} {F : Factory α} {c₁ : α} {c₂ : α} {c₃ : α} (h₁ : Factory.le F c₁ c₂ = true) (h₂ : Factory.lt F c₂ c₃) (h₃ : Factory.le F c₃ c₁ = true) : False