Fibers of a map restricted to a preimage

The fiber of Set.restrictPreimage over a point has the same cardinality as the corresponding fiber of the original map. Dually, removing the preimage of a set from the domain does not change the fibers over points outside that set.

@[simp]

theorem TauCeti.ncard_fiber_restrictPreimage {α : Type u_1} {β : Type u_2} (f : α → β) (t : Set β) (w : ↑t) : (t.restrictPreimage f ⁻¹' {w}).ncard = (f ⁻¹' {↑w}).ncard

Restricting a map to the preimage of a set does not change the cardinality of a fiber over a point of that set.

theorem TauCeti.natCard_fiber_sdiff_preimage {α : Type u_1} {β : Type u_2} (f : α → β) {T : Set α} {Z : Set β} {y : β} (hy : y ∉ Z) : Nat.card { x : α // f x = y ∧ x ∈ T \ f ⁻¹' Z } = Nat.card { x : α // f x = y ∧ x ∈ T }

Removing the preimage of a set Z from a set T does not change the cardinality of the part of T in a fiber over a point outside Z.