Skip to content

Commit

Permalink
doc: fix arrow direction in comment for PGame.le_trans_aux (#5509)
Browse files Browse the repository at this point in the history
  • Loading branch information
dwrensha committed Jun 27, 2023
1 parent a38feb8 commit f11fa33
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/SetTheory/Game/PGame.lean
Expand Up @@ -506,7 +506,7 @@ theorem lf_mk_of_le {x yl yr} {yL : yl → PGame} (yR) {i} : x ≤ yL i → x
@lf_of_le_moveLeft x (mk _ _ _ _) i
#align pgame.lf_mk_of_le PGame.lf_mk_of_le

/- We prove that `x ≤ y → y ≤ z x ≤ z` inductively, by also simultaneously proving its cyclic
/- We prove that `x ≤ y → y ≤ z x ≤ z` inductively, by also simultaneously proving its cyclic
reorderings. This auxiliary lemma is used during said induction. -/
private theorem le_trans_aux {x y z : PGame}
(h₁ : ∀ {i}, y ≤ z → z ≤ x.moveLeft i → y ≤ x.moveLeft i)
Expand Down

0 comments on commit f11fa33

Please sign in to comment.