Documentation

Lean 4 Proof

theorem cycle_product_monotone {N : ℕ} (k₁ k₂ : Fin N → ℝ)
    (hk₁_pos : ∀ n, 0 < k₁ n)
    (h_inc : ∀ n, k₁ n ≤ k₂ n)
    (h_strict : ∃ n, k₁ n < k₂ n) :
    ∏ n : Fin N, k₁ n < ∏ n : Fin N, k₂ n := by
  apply Finset.prod_lt_prod
    (fun n _ => hk₁_pos n) (fun n _ => h_inc n)
  obtain ⟨m, hm⟩ := h_strict
  exact ⟨m, Finset.mem_univ m, hm⟩

Dependency Graph

Location

thesis/CESProofs/Hierarchy/EndogenousCrossing.lean:242

Module Section

Proposition: Endogenous Crossing

In the same file