Let X, Tx, f and V be given.
Assume HTx: topology_on X Tx.
Assume HVopen: V ∈ Tx.
Assume Hzero: ∀x : set, x ∈ (X ∖ V) → apply_fun f x = 0.
We will prove support_of X Tx f ⊆ closure_of X Tx V.
We prove the intermediate claim HTsub: Tx ⊆ 𝒫 X.
An exact proof term for the current goal is (topology_subset_axiom X Tx HTx).
We prove the intermediate claim HVpow: V ∈ 𝒫 X.
An exact proof term for the current goal is (HTsub V HVopen).
We prove the intermediate claim HVsubX: V ⊆ X.
An exact proof term for the current goal is (PowerE X V HVpow).
Apply (support_of_sub_closure_of X Tx f V HTx HVsubX) to the current goal.
Let x be given.
Assume HxX: x ∈ X.
Assume Hnx0: apply_fun f x ≠ 0.
We will prove x ∈ V.
Apply (xm (x ∈ V)) to the current goal.
Assume HxV: x ∈ V.
An exact proof term for the current goal is HxV.
Assume Hxnot: ¬ (x ∈ V).
We prove the intermediate claim HxOut: x ∈ (X ∖ V).
An exact proof term for the current goal is (setminusI X V x HxX Hxnot).
We prove the intermediate claim Hx0: apply_fun f x = 0.
An exact proof term for the current goal is (Hzero x HxOut).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnx0 Hx0).
∎