Theorems · Theorem · logic and foundations

Set.mem_image_of_mem

∀ {α : Type u} {β : Type v} (f : α → β) {x : α} {a : Set α}, x ∈ a → f x ∈ f '' a

Defined in

Mathlib.Data.Set.Operations

Cited by

371 results in Mathlib

Foundations

Depth 5 from the axioms, rests on 12 definitions · uses no axioms