internlm/Lean-Github huggingface dataset:
Theorem: IsOpen.exists_mem_intrinsicInterior_convexHull_finset
Proof state before:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
hs : IsOpen (Subtype.val ⁻¹' s)
hx : x ∈ s
⊢ ∃ t, x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s
Tactic:
lift x to affineSpan ℝ s using subset_affineSpan _ _ hx
Proof state after:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen (Subtype.val ⁻¹' s)
x : ↥(affineSpan ℝ s)
hx : ↑x ∈ s
⊢ ∃ t, ↑x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s
Theorem: IsOpen.exists_mem_intrinsicInterior_convexHull_finset
Proof state before:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen (Subtype.val ⁻¹' s)
x : ↥(affineSpan ℝ s)
hx : ↑x ∈ s
⊢ ∃ t, ↑x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s
Tactic:
set x : affineSpan ℝ s := x with hx
Proof state after:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen (Subtype.val ⁻¹' s)
x✝ : ↥(affineSpan ℝ s)
x : ↥(affineSpan ℝ s) := x✝
hx✝ : ↑x ∈ s
hx : x = x✝
⊢ ∃ t, ↑x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s
Theorem: IsOpen.exists_mem_intrinsicInterior_convexHull_finset
Proof state before:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen (Subtype.val ⁻¹' s)
x✝ : ↥(affineSpan ℝ s)
x : ↥(affineSpan ℝ s) := x✝
hx✝ : ↑x ∈ s
hx : x = x✝
⊢ ∃ t, ↑x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s
Tactic:
clear_value x
Proof state after:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen (Subtype.val ⁻¹' s)
x✝ x : ↥(affineSpan ℝ s)
hx✝ : ↑x ∈ s
hx : x = x✝
⊢ ∃ t, ↑x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s
Theorem: IsOpen.exists_mem_intrinsicInterior_convexHull_finset
Proof state before:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen (Subtype.val ⁻¹' s)
x✝ x : ↥(affineSpan ℝ s)
hx✝ : ↑x ∈ s
hx : x = x✝
⊢ ∃ t, ↑x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s
Tactic:
subst hx
Proof state after:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen (Subtype.val ⁻¹' s)
x : ↥(affineSpan ℝ s)
hx : ↑x ∈ s
⊢ ∃ t, ↑x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s
Theorem: IsOpen.exists_mem_intrinsicInterior_convexHull_finset
Proof state before:
case intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen (Subtype.val ⁻¹' s)
x : ↥(affineSpan ℝ s)
hx : ↑x ∈ s
⊢ ∃ t, ↑x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s
Tactic:
obtain ⟨ε, hε, hεx⟩ := (Metric.nhds_basis_closedBall.1 _).1 (isOpen_iff_mem_nhds.1 hs _ hx)
Proof state after:
case intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen (Subtype.val ⁻¹' s)
x : ↥(affineSpan ℝ s)
hx : ↑x ∈ s
ε : ℝ
hε : 0 < ε
hεx : closedBall x ε ⊆ Subtype.val ⁻¹' s
⊢ ∃ t, ↑x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s
Theorem: IsOpen.exists_mem_intrinsicInterior_convexHull_finset
Proof state before:
case intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen (Subtype.val ⁻¹' s)
x : ↥(affineSpan ℝ s)
hx : ↑x ∈ s
ε : ℝ
hε : 0 < ε
hεx : closedBall x ε ⊆ Subtype.val ⁻¹' s
⊢ ∃ t, ↑x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s
Tactic:
set f : Finset (Fin $ finrank ℝ $ vectorSpan ℝ s) → vectorSpan ℝ s :=
  fun u ↦ (ε / ∑ i, ‖finBasis ℝ (vectorSpan ℝ s) i‖) • ∑ i, if i ∈ u then
    finBasis ℝ (vectorSpan ℝ s) i else -finBasis ℝ (vectorSpan ℝ s) i
    with hf
Proof state after:
case intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen (Subtype.val ⁻¹' s)
x : ↥(affineSpan ℝ s)
hx : ↑x ∈ s
ε : ℝ
hε : 0 < ε
hεx : closedBall x ε ⊆ Subtype.val ⁻¹' s
f : Finset (Fin (finrank ℝ ↥(vectorSpan ℝ s))) → ↥(vectorSpan ℝ s) :=
  fun u =>
    (ε / ∑ i : Fin (finrank ℝ ↥(vectorSpan ℝ s)), ‖(finBasis ℝ ↥(vectorSpan ℝ s)) i‖) •
      ∑ i : Fin (finrank ℝ ↥(vectorSpan ℝ s)),
        if i ∈ u then (finBasis ℝ ↥(vectorSpan ℝ s)) i else -(finBasis ℝ ↥(vectorSpan ℝ s)) i
hf :
  f = fun u =>
    (ε / ∑ i : Fin (finrank ℝ ↥(vectorSpan ℝ s)), ‖(finBasis ℝ ↥(vectorSpan ℝ s)) i‖) •
      ∑ i : Fin (finrank ℝ ↥(vectorSpan ℝ s)),
        if i ∈ u then (finBasis ℝ ↥(vectorSpan ℝ s)) i else -(finBasis ℝ ↥(vectorSpan ℝ s)) i
⊢ ∃ t, ↑x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s
Theorem: IsOpen.exists_mem_intrinsicInterior_convexHull_finset
Proof state before:
case intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
hs : IsOpen (Subtype.val ⁻¹' s)
x : ↥(affineSpan ℝ s)
hx : ↑x ∈ s
ε : ℝ
hε : 0 < ε
hεx : closedBall x ε ⊆ Subtype.val ⁻¹' s
f : Finset (Fin (finrank ℝ ↥(vectorSpan ℝ s))) → ↥(vectorSpan ℝ s) :=
  fun u =>
    (ε / ∑ i : Fin (finrank ℝ ↥(vectorSpan ℝ s)), ‖(finBasis ℝ ↥(vectorSpan ℝ s)) i‖) •
      ∑ i : Fin (finrank ℝ ↥(vectorSpan ℝ s)),
        if i ∈ u then (finBasis ℝ ↥(vectorSpan ℝ s)) i else -(finBasis ℝ ↥(vectorSpan ℝ s)) i
hf :
  f = fun u =>
    (ε / ∑ i : Fin (finrank ℝ ↥(vectorSpan ℝ s)), ‖(finBasis ℝ ↥(vectorSpan ℝ s)) i‖) •
      ∑ i : Fin (finrank ℝ ↥(vectorSpan ℝ s)),
        if i ∈ u then (finBasis ℝ ↥(vectorSpan ℝ s)) i else -(finBasis ℝ ↥(vectorSpan ℝ s)) i
⊢ ∃ t, ↑x ∈ intrinsicInterior ℝ ((convexHull ℝ) ↑t) ∧ (convexHull ℝ) ↑t ⊆ s
Tactic:
sorry
Proof state after:
no goals
Theorem: ConvexOn.continuousOn
Proof state before:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
f : E → ℝ
hf : ConvexOn ℝ s f
⊢ ContinuousOn f (intrinsicInterior ℝ s)
Tactic:
classical
sorry
Proof state after:
no goals
Theorem: ConvexOn.continuousOn
Proof state before:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
f : E → ℝ
hf : ConvexOn ℝ s f
⊢ ContinuousOn f (intrinsicInterior ℝ s)
Tactic:
sorry
Proof state after:
no goals
Theorem: Nat.prime_composite_induction
Proof state before:
P : ℕ → Prop
zero : P 0
one : P 1
prime : ∀ (p : ℕ), p.Prime → P p
composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)
n : ℕ
⊢ P n
Tactic:
refine induction_on_primes zero one ?_ _
Proof state after:
P : ℕ → Prop
zero : P 0
one : P 1
prime : ∀ (p : ℕ), p.Prime → P p
composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)
n : ℕ
⊢ ∀ (p a : ℕ), p.Prime → P a → P (p * a)
Theorem: Nat.prime_composite_induction
Proof state before:
P : ℕ → Prop
zero : P 0
one : P 1
prime : ∀ (p : ℕ), p.Prime → P p
composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)
n : ℕ
⊢ ∀ (p a : ℕ), p.Prime → P a → P (p * a)
Tactic:
rintro p (_ | _ | a) hp ha
Proof state after:
case zero
P : ℕ → Prop
zero : P 0
one : P 1
prime : ∀ (p : ℕ), p.Prime → P p
composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)
n p : ℕ
hp : p.Prime
ha : P 0
⊢ P (p * 0)

case succ.zero
P : ℕ → Prop
zero : P 0
one : P 1
prime : ∀ (p : ℕ), p.Prime → P p
composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)
n p : ℕ
hp : p.Prime
ha : P (0 + 1)
⊢ P (p * (0 + 1))

case succ.succ
P : ℕ → Prop
zero : P 0
one : P 1
prime : ∀ (p : ℕ), p.Prime → P p
composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)
n p a : ℕ
hp : p.Prime
ha : P (a + 1 + 1)
⊢ P (p * (a + 1 + 1))
Theorem: Nat.prime_composite_induction
Proof state before:
case zero
P : ℕ → Prop
zero : P 0
one : P 1
prime : ∀ (p : ℕ), p.Prime → P p
composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)
n p : ℕ
hp : p.Prime
ha : P 0
⊢ P (p * 0)
Tactic:
simpa
Proof state after:
no goals
Theorem: Nat.prime_composite_induction
Proof state before:
case succ.zero
P : ℕ → Prop
zero : P 0
one : P 1
prime : ∀ (p : ℕ), p.Prime → P p
composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)
n p : ℕ
hp : p.Prime
ha : P (0 + 1)
⊢ P (p * (0 + 1))
Tactic:
simpa using prime _ hp
Proof state after:
no goals
Theorem: Nat.prime_composite_induction
Proof state before:
case succ.succ
P : ℕ → Prop
zero : P 0
one : P 1
prime : ∀ (p : ℕ), p.Prime → P p
composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)
n p a : ℕ
hp : p.Prime
ha : P (a + 1 + 1)
⊢ P (p * (a + 1 + 1))
Tactic:
exact composite _ hp.two_le (prime _ hp) _ a.one_lt_succ_succ ha
Proof state after:
no goals
Theorem: IncidenceAlgebra.ext
Proof state before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝¹ : Zero 𝕜
inst✝ : LE α
a b : α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → f a b = g a b
⊢ f = g
Tactic:
refine' DFunLike.coe_injective' (funext₂ fun a b ↦ _)
Proof state after:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝¹ : Zero 𝕜
inst✝ : LE α
a✝ b✝ : α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → f a b = g a b
a b : α
⊢ f a b = g a b
Theorem: IncidenceAlgebra.ext
Proof state before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝¹ : Zero 𝕜
inst✝ : LE α
a✝ b✝ : α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → f a b = g a b
a b : α
⊢ f a b = g a b
Tactic:
by_cases hab : a ≤ b
Proof state after:
case pos
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝¹ : Zero 𝕜
inst✝ : LE α
a✝ b✝ : α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → f a b = g a b
a b : α
hab : a ≤ b
⊢ f a b = g a b

case neg
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝¹ : Zero 𝕜
inst✝ : LE α
a✝ b✝ : α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → f a b = g a b
a b : α
hab : ¬a ≤ b
⊢ f a b = g a b
Theorem: IncidenceAlgebra.ext
Proof state before:
case pos
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝¹ : Zero 𝕜
inst✝ : LE α
a✝ b✝ : α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → f a b = g a b
a b : α
hab : a ≤ b
⊢ f a b = g a b
Tactic:
exact h _ _ hab
Proof state after:
no goals
Theorem: IncidenceAlgebra.ext
Proof state before:
case neg
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝¹ : Zero 𝕜
inst✝ : LE α
a✝ b✝ : α
f g : IncidenceAlgebra 𝕜 α
h : ∀ (a b : α), a ≤ b → f a b = g a b
a b : α
hab : ¬a ≤ b
⊢ f a b = g a b
Tactic:
rw [apply_eq_zero_of_not_le hab, apply_eq_zero_of_not_le hab]
Proof state after:
no goals
Theorem: IncidenceAlgebra.zeta_mul_zeta
Proof state before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝³ : Semiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b : α
⊢ (zeta 𝕜 * zeta 𝕜) a b = ↑(Icc a b).card
Tactic:
rw [mul_apply, card_eq_sum_ones, Nat.cast_sum, Nat.cast_one]
Proof state after:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝³ : Semiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b : α
⊢ ∑ x ∈ Icc a b, (zeta 𝕜) a x * (zeta 𝕜) x b = ∑ x ∈ Icc a b, 1
Theorem: IncidenceAlgebra.zeta_mul_zeta
Proof state before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝³ : Semiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b : α
⊢ ∑ x ∈ Icc a b, (zeta 𝕜) a x * (zeta 𝕜) x b = ∑ x ∈ Icc a b, 1
Tactic:
refine' sum_congr rfl fun x hx ↦ _
Proof state after:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝³ : Semiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b x : α
hx : x ∈ Icc a b
⊢ (zeta 𝕜) a x * (zeta 𝕜) x b = 1
Theorem: IncidenceAlgebra.zeta_mul_zeta
Proof state before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝³ : Semiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b x : α
hx : x ∈ Icc a b
⊢ (zeta 𝕜) a x * (zeta 𝕜) x b = 1
Tactic:
rw [mem_Icc] at hx
Proof state after:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝³ : Semiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b x : α
hx : a ≤ x ∧ x ≤ b
⊢ (zeta 𝕜) a x * (zeta 𝕜) x b = 1
Theorem: IncidenceAlgebra.zeta_mul_zeta
Proof state before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝³ : Semiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b x : α
hx : a ≤ x ∧ x ≤ b
⊢ (zeta 𝕜) a x * (zeta 𝕜) x b = 1
Tactic:
rw [zeta_of_le hx.1, zeta_of_le hx.2, one_mul]
Proof state after:
no goals
Theorem: IncidenceAlgebra.zeta_mul_kappa
Proof state before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝³ : Semiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b : α
⊢ (zeta 𝕜 * zeta 𝕜) a b = ↑(Icc a b).card
Tactic:
rw [mul_apply, card_eq_sum_ones, Nat.cast_sum, Nat.cast_one]
Proof state after:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝³ : Semiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b : α
⊢ ∑ x ∈ Icc a b, (zeta 𝕜) a x * (zeta 𝕜) x b = ∑ x ∈ Icc a b, 1
Theorem: IncidenceAlgebra.zeta_mul_kappa
Proof state before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝³ : Semiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b : α
⊢ ∑ x ∈ Icc a b, (zeta 𝕜) a x * (zeta 𝕜) x b = ∑ x ∈ Icc a b, 1
Tactic:
refine' sum_congr rfl fun x hx ↦ _
Proof state after:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝³ : Semiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b x : α
hx : x ∈ Icc a b
⊢ (zeta 𝕜) a x * (zeta 𝕜) x b = 1
Theorem: IncidenceAlgebra.zeta_mul_kappa
Proof state before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝³ : Semiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b x : α
hx : x ∈ Icc a b
⊢ (zeta 𝕜) a x * (zeta 𝕜) x b = 1
Tactic:
rw [mem_Icc] at hx
Proof state after:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝³ : Semiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b x : α
hx : a ≤ x ∧ x ≤ b
⊢ (zeta 𝕜) a x * (zeta 𝕜) x b = 1
Theorem: IncidenceAlgebra.zeta_mul_kappa
Proof state before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝³ : Semiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b x : α
hx : a ≤ x ∧ x ≤ b
⊢ (zeta 𝕜) a x * (zeta 𝕜) x b = 1
Tactic:
rw [zeta_of_le hx.1, zeta_of_le hx.2, one_mul]
Proof state after:
no goals
Theorem: IncidenceAlgebra.muAux_apply
Proof state before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ muAux 𝕜 a b = if a = b then 1 else -∑ x ∈ (Ico a b).attach, muAux 𝕜 a ↑x
Tactic:
rw [muAux]
Proof state after:
no goals
Theorem: IncidenceAlgebra.mu_apply
Proof state before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ (mu 𝕜) a b = if a = b then 1 else -∑ x ∈ Ico a b, (mu 𝕜) a x
Tactic:
rw [mu, coe_mk, muAux_apply, sum_attach]
Proof state after:
no goals
Theorem: IncidenceAlgebra.mu_apply_of_eq
Proof state before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a = b
⊢ (mu 𝕜) a b = 1
Tactic:
rw [mu_apply, if_pos h]
Proof state after:
no goals
Theorem: IncidenceAlgebra.mu_apply_of_ne
Proof state before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
⊢ (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
Tactic:
rw [mu_apply, if_neg h]
Proof state after:
no goals
Theorem: IncidenceAlgebra.mu_spec_of_ne_right
Proof state before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 0
Tactic:
have : mu 𝕜 a b = _ := mu_apply_of_ne h
Proof state after:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 0
Theorem: IncidenceAlgebra.mu_spec_of_ne_right
Proof state before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 0
Tactic:
by_cases hab : a ≤ b
Proof state after:
case pos
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
hab : a ≤ b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 0

case neg
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
hab : ¬a ≤ b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 0
Theorem: IncidenceAlgebra.mu_spec_of_ne_right
Proof state before:
case pos
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
hab : a ≤ b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 0
Tactic:
rw [Icc_eq_cons_Ico hab]
Proof state after:
case pos
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
hab : a ≤ b
⊢ ∑ x ∈ cons b (Ico a b) ⋯, (mu 𝕜) a x = 0
Theorem: IncidenceAlgebra.mu_spec_of_ne_right
Proof state before:
case pos
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
hab : a ≤ b
⊢ ∑ x ∈ cons b (Ico a b) ⋯, (mu 𝕜) a x = 0
Tactic:
simp [this, neg_add_self]
Proof state after:
no goals
Theorem: IncidenceAlgebra.mu_spec_of_ne_right
Proof state before:
case neg
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
hab : ¬a ≤ b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 0
Tactic:
have : ∀ x ∈ Icc a b, ¬a ≤ x := by
  intro x hx hn
  apply hab
  rw [mem_Icc] at hx
  exact le_trans hn hx.2
Proof state after:
case neg
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this✝ : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
hab : ¬a ≤ b
this : ∀ x ∈ Icc a b, ¬a ≤ x
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 0
Theorem: IncidenceAlgebra.mu_spec_of_ne_right
Proof state before:
case neg
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this✝ : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
hab : ¬a ≤ b
this : ∀ x ∈ Icc a b, ¬a ≤ x
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 0
Tactic:
convert sum_const_zero
Proof state after:
case h.e'_2.a
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this✝ : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
hab : ¬a ≤ b
this : ∀ x ∈ Icc a b, ¬a ≤ x
x✝ : α
a✝ : x✝ ∈ Icc a b
⊢ (mu 𝕜) a x✝ = 0
Theorem: IncidenceAlgebra.mu_spec_of_ne_right
Proof state before:
case h.e'_2.a
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this✝ : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
hab : ¬a ≤ b
this : ∀ x ∈ Icc a b, ¬a ≤ x
x✝ : α
a✝ : x✝ ∈ Icc a b
⊢ (mu 𝕜) a x✝ = 0
Tactic:
simp [apply_eq_zero_of_not_le (this ‹_› ‹_›)]
Proof state after:
no goals
Theorem: IncidenceAlgebra.mu_spec_of_ne_right
Proof state before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
hab : ¬a ≤ b
⊢ ∀ x ∈ Icc a b, ¬a ≤ x
Tactic:
intro x hx hn
Proof state after:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
hab : ¬a ≤ b
x : α
hx : x ∈ Icc a b
hn : a ≤ x
⊢ False
Theorem: IncidenceAlgebra.mu_spec_of_ne_right
Proof state before:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
hab : ¬a ≤ b
x : α
hx : x ∈ Icc a b
hn : a ≤ x
⊢ False
Tactic:
apply hab
Proof state after:
𝕄 : Type u_1
F : Type u_2
𝕜 : Type u_3
𝕝 : Type u_4
𝕞 : Type u_5
α : Type u_6
β : Type u_7
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
this : (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x
hab : ¬a ≤ b
x : α
hx : x ∈ Icc a b
hn : a ≤ x
⊢ a ≤ b