English
An induction principle for pairs of ereals that splits on signs when infinities occur, with a premise allowing negation on the left and a base/step cover. This is a structured elimination principle to reason about two-argument predicates on EReal.
Русский
Принцип индукции по двум вещественным бесконечностям с разбиением по знаку при бесконечности слева, допускающий отрицание слева и базовые/шаговые случаи; удобный инструмент для анализа предикатов на паре ereal.
LaTeX
$$$\text{Induction₂_neg_left} := \text{(ивент)}$$$
Lean4
/-- Induct on two ereals by performing case splits on the sign of one whenever the other is
infinite. This version eliminates some cases by assuming that `P x y` implies `P (-x) y` for all
`x`, `y`. -/
@[elab_as_elim]
theorem induction₂_neg_left {P : EReal → EReal → Prop} (neg_left : ∀ {x y}, P x y → P (-x) y) (top_top : P ⊤ ⊤)
(top_pos : ∀ x : ℝ, 0 < x → P ⊤ x) (top_zero : P ⊤ 0) (top_neg : ∀ x : ℝ, x < 0 → P ⊤ x) (top_bot : P ⊤ ⊥)
(zero_top : P 0 ⊤) (zero_bot : P 0 ⊥) (pos_top : ∀ x : ℝ, 0 < x → P x ⊤) (pos_bot : ∀ x : ℝ, 0 < x → P x ⊥)
(coe_coe : ∀ x y : ℝ, P x y) : ∀ x y, P x y :=
have : ∀ y, (∀ x : ℝ, 0 < x → P x y) → ∀ x : ℝ, x < 0 → P x y := fun _ h x hx =>
neg_neg (x : EReal) ▸ neg_left <| h _ (neg_pos_of_neg hx)
@induction₂ P top_top top_pos top_zero top_neg top_bot pos_top pos_bot zero_top coe_coe zero_bot (this _ pos_top)
(this _ pos_bot) (neg_left top_top) (fun x hx => neg_left <| top_pos x hx) (neg_left top_zero)
(fun x hx => neg_left <| top_neg x hx) (neg_left top_bot)
