Commit 2023-09-10 03:26 4a238556

View on Github →

chore: tidy various files (#7041)

Estimated changes

Modified Mathlib/Data/Finset/LocallyFinite.lean

Modified Mathlib/Data/Seq/Computation.lean

deleted theorem Computation.LiftRelAux_inl_inl

deleted theorem Computation.LiftRelAux_inl_inr

deleted theorem Computation.LiftRelAux_inr_inl

deleted theorem Computation.LiftRelAux_inr_inr

added theorem Computation.empty_orElse

deleted theorem Computation.empty_orelse

deleted theorem Computation.exists_of_LiftRel_left

deleted theorem Computation.exists_of_LiftRel_right

added theorem Computation.exists_of_liftRel_left

added theorem Computation.exists_of_liftRel_right

added theorem Computation.liftRelAux_inl_inl

added theorem Computation.liftRelAux_inl_inr

added theorem Computation.liftRelAux_inr_inl

added theorem Computation.liftRelAux_inr_inr

added theorem Computation.liftRel_rec

deleted theorem Computation.lift_rel_rec

added theorem Computation.orElse_empty

added theorem Computation.orElse_pure

added theorem Computation.orElse_think

deleted theorem Computation.orelse_empty

deleted theorem Computation.orelse_pure

deleted theorem Computation.orelse_think

deleted theorem Computation.rel_of_LiftRel

added theorem Computation.rel_of_liftRel

deleted theorem Computation.terminates_of_LiftRel

added theorem Computation.terminates_of_liftRel

Modified Mathlib/Data/Seq/WSeq.lean

Modified Mathlib/MeasureTheory/Integral/Bochner.lean

Modified Mathlib/Topology/Sheaves/SheafCondition/OpensLeCover.lean