mem_image₂_iff — Mathlib

English

If f is injective in both arguments, then f a b ∈ image₂ f s t iff a ∈ s and b ∈ t.

Русский

Если f инъективна по обоим аргументам, то f(a,b) ∈ image₂ f S T тогда и только тогда, когда a ∈ S и b ∈ T.

LaTeX

$$mem_image₂_iff (hf) : f a b ∈ image₂ f s t ↔ a ∈ s ∧ b ∈ t$$

Lean4

theorem mem_image₂_iff (hf : Injective2 f) : f a b ∈ image₂ f s t ↔ a ∈ s ∧ b ∈ t := by
  rw [← mem_coe, coe_image₂, mem_image2_iff hf, mem_coe, mem_coe]

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