teorth
diff --git a/‎Analysis/MeasureTheory/Section_1_4_3.lean‎
Lines changed: 2 additions & 1 deletion b/‎Analysis/MeasureTheory/Section_1_4_3.lean‎
Lines changed: 2 additions & 1 deletion
@@ -123,7 +123,8 @@ noncomputable def FinitelyAdditiveMeasure.counting (X:Type*) : FinitelyAdditiveM
     measure := fun E => ENat.card E
     measure_pos := by sorry
     measure_empty := by sorry
-    measure_finite_additive := by sorry
+    measure_finite_additive := fun E F _ _ hdisj =>
+      (ENat.card_union_eq_add_card_of_disjoint hdisj).symm
   }
 
 /-- Exercise 1.4.20(i) -/
Original file line number	Diff line number	Diff line change
`@@ -123,7 +123,8 @@ noncomputable def FinitelyAdditiveMeasure.counting (X:Type*) : FinitelyAdditiveM`
`123`	`123`	`measure := fun E => ENat.card E`
`124`	`124`	`measure_pos := by sorry`
`125`	`125`	`measure_empty := by sorry`
`126`		`- measure_finite_additive := by sorry`
	`126`	`+ measure_finite_additive := fun E F _ _ hdisj =>`
	`127`	`+ (ENat.card_union_eq_add_card_of_disjoint hdisj).symm`
`127`	`128`	`}`
`128`	`129`
`129`	`130`	`/-- Exercise 1.4.20(i) -/`