Let X, Tx and F be given.
Assume HTx: topology_on X Tx.
Assume HFfin: finite F.
Assume HFsubPow: F ⊆ 𝒫 X.
We will prove locally_finite_family X Tx F.
We will prove topology_on X Tx ∧ ∀x : set, x ∈ X → ∃N : set, N ∈ Tx ∧ x ∈ N ∧ ∃S : set, finite S ∧ S ⊆ F ∧ ∀A : set, A ∈ F → A ∩ N ≠ Empty → A ∈ S.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Let x be given.
Assume HxX: x ∈ X.
We use X to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (topology_has_X X Tx HTx).
An exact proof term for the current goal is HxX.
We use F to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HFfin.
An exact proof term for the current goal is (Subq_ref F).
Let A be given.
Assume HA: A ∈ F.
Assume _.
An exact proof term for the current goal is HA.
∎