image2_right — Mathlib

English

Let s ⊆ α. If the second argument is the identity on the second variable, then image2 (λ _ y => y) s t = t for any t ⊆ β, provided s is nonempty.

Русский

Пусть s ⊆ α. Пусть функция во второй аргумент отдаёт этот второй аргумент. Тогда image2 (λ _ y. y) s t = t при любом t ⊆ β и непустом s.

LaTeX

$$$\\text{If } s \\neq \\varnothing,\\quad \\operatorname{image}_2(\\lambda _ y . y)\\, s\\, t = t$$$

Lean4

@[simp]
theorem image2_right (h : s.Nonempty) : image2 (fun _ y => y) s t = t := by simp [nonempty_def.mp h, Set.ext_iff]

Похожие утверждения