English
An elimination principle for two EReal arguments: to prove a property P(x,y) for all x,y in EReal, it suffices to verify a collection of base cases and how P propagates through the finite (real) parts and infinities.
Русский
Классический метод эллиминации для пары элементов EReal: чтобы доказать свойство P(x,y) для всех x,y ∈ EReal, достаточно проверить набор базовых случаев и то, как P переносится между конечной (действительной) частью и бесконечностями.
LaTeX
$$$\forall x,y\in \mathrm{EReal},\ P(x,y)$, где P удовлетворяет указанным базовым условиям и переходам между случаями.$$
Lean4
/-- Induct on two `EReal`s by performing case splits on the sign of one whenever the other is
infinite. -/
@[elab_as_elim]
theorem induction₂ {P : EReal → EReal → Prop} (top_top : P ⊤ ⊤) (top_pos : ∀ x : ℝ, 0 < x → P ⊤ x) (top_zero : P ⊤ 0)
(top_neg : ∀ x : ℝ, x < 0 → P ⊤ x) (top_bot : P ⊤ ⊥) (pos_top : ∀ x : ℝ, 0 < x → P x ⊤)
(pos_bot : ∀ x : ℝ, 0 < x → P x ⊥) (zero_top : P 0 ⊤) (coe_coe : ∀ x y : ℝ, P x y) (zero_bot : P 0 ⊥)
(neg_top : ∀ x : ℝ, x < 0 → P x ⊤) (neg_bot : ∀ x : ℝ, x < 0 → P x ⊥) (bot_top : P ⊥ ⊤)
(bot_pos : ∀ x : ℝ, 0 < x → P ⊥ x) (bot_zero : P ⊥ 0) (bot_neg : ∀ x : ℝ, x < 0 → P ⊥ x) (bot_bot : P ⊥ ⊥) :
∀ x y, P x y
| ⊥, ⊥ => bot_bot
| ⊥, (y : ℝ) => by
rcases lt_trichotomy y 0 with (hy | rfl | hy)
exacts [bot_neg y hy, bot_zero, bot_pos y hy]
| ⊥, ⊤ => bot_top
| (x : ℝ), ⊥ => by
rcases lt_trichotomy x 0 with (hx | rfl | hx)
exacts [neg_bot x hx, zero_bot, pos_bot x hx]
| (x : ℝ), (y : ℝ) => coe_coe _ _
| (x : ℝ), ⊤ => by
rcases lt_trichotomy x 0 with (hx | rfl | hx)
exacts [neg_top x hx, zero_top, pos_top x hx]
| ⊤, ⊥ => top_bot
| ⊤, (y : ℝ) => by
rcases lt_trichotomy y 0 with (hy | rfl | hy)
exacts [top_neg y hy, top_zero, top_pos y hy]
| ⊤, ⊤ => top_top
