Interiors and fibres in product spaces

A subset of a product has empty interior if all its vertical fibres have empty interior. This lets fibrewise empty-interior results apply to subsets of arbitrary topological products, without countability, separation, or finite-dimensionality assumptions on either factor. In particular, graphs with values in a space without isolated points have empty interior.

theorem TauCeti.coe_sumArrowHomeomorphProdArrow {X : Type u_1} {ι : Type u_2} {ι' : Type u_3} [TopologicalSpace X] : ⇑Homeomorph.sumArrowHomeomorphProdArrow = ⇑(Equiv.sumArrowEquivProdArrow ι ι' X)

The sum-to-product homeomorphism has the same underlying function as the corresponding coordinate equivalence.

theorem TauCeti.interior_eq_empty_of_forall_interior_preimage_prodMk_eq_empty {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set (X × Y)} (hs : ∀ (x : X), interior (Prod.mk x ⁻¹' s) = ∅) : interior s = ∅

A subset of a product has empty interior if every vertical fibre has empty interior.

@[simp]

theorem Set.interior_graphOn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [∀ (y : Y), (nhdsWithin y {y}ᶜ).NeBot] (s : Set X) (f : X → Y) : interior (graphOn f s) = ∅

A graph with values in a space without isolated points has empty interior, even when neither the function nor its domain is open or continuous.