Commit 2023-02-11 07:51 f7cd1dc5

View on Github →

feat: port Topology.Sets.Opens (#2118)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Sets/Opens.lean

added def Homeomorph.opensCongr

added theorem Homeomorph.opensCongr_symm

added theorem TopologicalSpace.OpenNhdsOf.basis_nhds

added def TopologicalSpace.OpenNhdsOf.comap

added theorem TopologicalSpace.OpenNhdsOf.toOpens_injective

added structure TopologicalSpace.OpenNhdsOf

added theorem TopologicalSpace.Opens.IsBasis.isCompact_open_iff_eq_finite_unionᵢ

added def TopologicalSpace.Opens.IsBasis

added def TopologicalSpace.Opens.Simps.coe

added theorem TopologicalSpace.Opens.carrier_eq_coe

added theorem TopologicalSpace.Opens.coe_bot

added theorem TopologicalSpace.Opens.coe_comap

added theorem TopologicalSpace.Opens.coe_eq_empty

added theorem TopologicalSpace.Opens.coe_eq_univ

added theorem TopologicalSpace.Opens.coe_finset_inf

added theorem TopologicalSpace.Opens.coe_finset_sup

added theorem TopologicalSpace.Opens.coe_inf

added theorem TopologicalSpace.Opens.coe_inj

added theorem TopologicalSpace.Opens.coe_mk

added theorem TopologicalSpace.Opens.coe_sup

added theorem TopologicalSpace.Opens.coe_supᵢ

added theorem TopologicalSpace.Opens.coe_supₛ

added theorem TopologicalSpace.Opens.coe_top

added def TopologicalSpace.Opens.comap

added theorem TopologicalSpace.Opens.comap_id

added theorem TopologicalSpace.Opens.comap_injective

added theorem TopologicalSpace.Opens.comap_mono

added theorem TopologicalSpace.Opens.eq_bot_or_top

added theorem TopologicalSpace.Opens.ext

added theorem TopologicalSpace.Opens.gc

added def TopologicalSpace.Opens.gi

added theorem TopologicalSpace.Opens.isBasis_iff_cover

added theorem TopologicalSpace.Opens.isBasis_iff_nbhd

added theorem TopologicalSpace.Opens.isCompactElement_iff

added theorem TopologicalSpace.Opens.mem_mk

added theorem TopologicalSpace.Opens.mem_supᵢ

added theorem TopologicalSpace.Opens.mem_supₛ

added theorem TopologicalSpace.Opens.mk_coe

added theorem TopologicalSpace.Opens.mk_inf_mk

added theorem TopologicalSpace.Opens.ne_bot_iff_nonempty

added theorem TopologicalSpace.Opens.not_nonempty_iff_eq_bot

added theorem TopologicalSpace.Opens.openEmbedding_of_le

added theorem TopologicalSpace.Opens.supᵢ_def

added theorem TopologicalSpace.Opens.supᵢ_mk

added theorem TopologicalSpace.Opens.«forall»

added structure TopologicalSpace.Opens