Theorems · Theorem · order theory

Set.subsingleton_of_image

∀ {α : Type u_1} {β : Type u_2} {f : α → β},
  Function.Injective f → ∀ (s : Set α), (f '' s).Subsingleton → s.Subsingleton

If the image of a set under an injective map is a subsingleton, the set is a subsingleton.

Defined in

Mathlib.Data.Set.Image

Cited by

3 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms