Theorems · Theorem · order theory

Set.image2_subset

∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s s' : Set α} {t t' : Set β},
  s ⊆ s' → t ⊆ t' → Set.image2 f s t ⊆ Set.image2 f s' t'

image2 is monotone with respect to ⊆.

Defined in

Mathlib.Data.Set.NAry

Cited by

25 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms