English
image2 is monotone with respect to ⊆ in both arguments: if s ⊆ s' and t ⊆ t' then image2 f s t ⊆ image2 f s' t'.
Русский
image2 монотонна по отношению к ⊆ по обеим аргументам: если s ⊆ s' и t ⊆ t', то image2 f s t ⊆ image2 f s' t'.
LaTeX
$$If s ⊆ s' and t ⊆ t', then image2 f s t ⊆ image2 f s' t'.$$
Lean4
/-- image2 is monotone with respect to `⊆`. -/
@[gcongr]
theorem image2_subset (hs : s ⊆ s') (ht : t ⊆ t') : image2 f s t ⊆ image2 f s' t' :=
by
rintro _ ⟨a, ha, b, hb, rfl⟩
exact mem_image2_of_mem (hs ha) (ht hb)