ι : Type u_1
ι' : Type ?u.14374
α : Type ?u.14377
X : Type u_2
Y : Type ?u.14383
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
f : Option ι → Set X
⊢ LocallyFinite ((f ∘ ↑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl) ∧
      LocallyFinite ((f ∘ ↑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inr) ↔
    LocallyFinite (f ∘ some)
ι : Type u_1
ι' : Type ?u.14374
α : Type ?u.14377
X : Type u_2
Y : Type ?u.14383
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
f : Option ι → Set X
⊢ LocallyFinite f ↔ LocallyFinite (f ∘ some)
rw [← (Equiv.optionEquivSumPUnit.{_, 0} ι).symm.locallyFinite_comp_iff, locallyFinite_sum]
ι : Type u_1
ι' : Type ?u.14374
α : Type ?u.14377
X : Type u_2
Y : Type ?u.14383
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
f : Option ι → Set X
⊢ LocallyFinite ((f ∘ ↑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl) ↔ LocallyFinite (f ∘ some)
ι : Type u_1
ι' : Type ?u.14374
α : Type ?u.14377
X : Type u_2
Y : Type ?u.14383
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
f : Option ι → Set X
⊢ LocallyFinite ((f ∘ ↑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl) ∧
      LocallyFinite ((f ∘ ↑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inr) ↔
    LocallyFinite (f ∘ some)
simp only [locallyFinite_of_finite, and_true]
no goals
ι : Type u_1
ι' : Type ?u.14374
α : Type ?u.14377
X : Type u_2
Y : Type ?u.14383
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f✝ g : ι → Set X
f : Option ι → Set X
⊢ LocallyFinite ((f ∘ ↑(Equiv.optionEquivSumPUnit ι).symm) ∘ Sum.inl) ↔ LocallyFinite (f ∘ some)
rfl