imc_equality_template

formal source

  44
  45    Given: (A) | (B) and (B) | (A) in a commutative ring,
  46    conclude (A) = (B) as principal ideals. -/
  47theorem imc_equality_template {R : Type*} [CommRing R]
  48    {A B : R} (hAB : A ∣ B) (hBA : B ∣ A) :
  49    Ideal.span ({A} : Set R) = Ideal.span {B} :=
  50  principal_ideal_eq_of_mutual_dvd hAB hBA
  51
  52/-! ## §3. Fredholm / operator pinch template -/
  53
  54/-- **F5.3.2**: A function that is not surjective cannot map finite sets
  55    onto infinite sets. (Basic set-theoretic obstruction.)
  56    This is the finite-capacity veto in its simplest form. -/
  57theorem finite_not_onto_infinite {α β : Type*} (f : α → β)
  58    [Finite α] (hβ : Infinite β) : ¬Function.Surjective f := by
  59  intro hsurj
  60  have : Finite β := Finite.of_surjective f hsurj
  61  exact not_finite β
  62
  63/-- **F5.3.1/3.2**: If the cost per operation is positive and the budget is finite,
  64    only finitely many operations can be performed. -/
  65theorem finite_operations_from_budget {n : ℕ} {cost budget : ℝ}
  66    (hcost : 0 < cost) (hbudget : 0 ≤ budget)
  67    (hfit : n * cost ≤ budget) :
  68    (n : ℝ) ≤ budget / cost := by
  69  rwa [le_div_iff₀ hcost]
  70
  71end PinchAlgebra
  72end Foundation
  73end IndisputableMonolith