# Cardinality of Image of Mapping of Intersections is not greater than Weight of Space

Jump to navigation
Jump to search

## Theorem

Let $T = \struct {X, \tau}$ be a topological space.

Let $f: X \to \tau$ be a mapping such that:

- $\forall x \in X: \paren {x \in \map f x \land \forall U \in \tau: x \in U \implies \map f x \subseteq U}$

Then the cardinality of the image of $f$ is no greater than the weight of $T$:

$\card {\Img f} \le \map w T$.

## Proof

By definition of weight there exists a basis $\BB$ of $T$ such that.

- $\card \BB = \map w T$

By Image of Mapping of Intersections is Smallest Basis:

- $\Img f \subseteq \BB$

Thus by Subset implies Cardinal Inequality:

- $\card {\Img f} \le \card \BB = \map w T$

$\blacksquare$

## Sources

- Mizar article TOPGEN_2:17