Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ereal.induction₂

Modification history

2023-02-24 10:27
src/data/real/ereal.lean
refactor(data/real/ereal): add a two-argument induction principle (#18481) …
Added ereal.induction₂View on Github →