English
A symmetric variant of induction₂: if the relation P is symmetric and satisfies the base cases, then P holds for all pairs x,y in EReal.
Русский
У симметричного варианта индукции₂: если отношение P симметрично и выполняются базовые случаи, то P выполняется для всех пар x,y в EReal.
LaTeX
$$$\forall {P: \mathrm{EReal} \to \mathrm{EReal} \to \mathrm{Prop}},\ (\forall x,y, P(x,y) \Rightarrow P(y,x)) \Rightarrow P(\top,\top) \Rightarrow \cdots \Rightarrow \forall x,y, P(x,y).$$$
Lean4
/-- Induct on two `EReal`s by performing case splits on the sign of one whenever the other is
infinite. This version eliminates some cases by assuming that the relation is symmetric. -/
@[elab_as_elim]
theorem induction₂_symm {P : EReal → EReal → Prop} (symm : ∀ {x y}, P x y → P y x) (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_bot : ∀ x : ℝ, 0 < x → P x ⊥) (coe_coe : ∀ x y : ℝ, P x y) (zero_bot : P 0 ⊥)
(neg_bot : ∀ x : ℝ, x < 0 → P x ⊥) (bot_bot : P ⊥ ⊥) : ∀ x y, P x y :=
@induction₂ P top_top top_pos top_zero top_neg top_bot (fun _ h => symm <| top_pos _ h) pos_bot (symm top_zero)
coe_coe zero_bot (fun _ h => symm <| top_neg _ h) neg_bot (symm top_bot) (fun _ h => symm <| pos_bot _ h)
(symm zero_bot) (fun _ h => symm <| neg_bot _ h) bot_bot
