class PiBase.TopologicalNManifoldWithBoundary (X : Type u) [TopologicalSpace X] extends SecondCountableTopology X, T2Space X, PiBase.LocallyNEuclideanHalfSpace X : Prop

• is_open_generated_countable : ∃ (b : Set (Set X)), b.Countable ∧ inst✝ = TopologicalSpace.generateFrom b
• t2 : Pairwise fun (x y : X) => ∃ (u : Set X) (v : Set X), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
• locally_homeomorph : ∃ (n : ℕ), ∀ (x : X), ∃ U ∈ nhds x, ∃ (f : ↑U → Fin n → NNReal), Topology.IsOpenEmbedding f