Skip to content

Commit 470e6da

Browse files
CoolRmalEtienneC30
andauthored
Update Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com>
1 parent d30739f commit 470e6da

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

  • Mathlib/MeasureTheory/Function/StronglyMeasurable

Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -793,7 +793,7 @@ protected theorem _root_.IndexedPartition.stronglyMeasurable_piecewise {s : ι
793793
fun x => ?_⟩
794794
simp [SimpleFunc.indexedPartitionPiecewise, IndexedPartition.piecewise_apply,
795795
StronglyMeasurable.tendsto_approx]
796-
· simp only [not_finite_iff_infinite] at Fi
796+
simp only [not_finite_iff_infinite] at Fi
797797
obtain ⟨e, -⟩ := exists_true_iff_nonempty.mpr (nonempty_equiv_of_countable (α := ℕ) (β := ι))
798798
have he := e.bijective
799799
classical

0 commit comments

Comments
 (0)