mem_image2_iff — Mathlib

English

If f is injective on pairs (Injective2 f), then f a b ∈ image2 f s t iff a ∈ s and b ∈ t.

Русский

Если f инъективна по парам (Injective2 f), то f a b ∈ image2 f s t эквивалентно a ∈ s и b ∈ t.

LaTeX

$$Injective2 f → (f a b ∈ image2 f s t ↔ a ∈ s ∧ b ∈ t).$$

Lean4

theorem mem_image2_iff (hf : Injective2 f) : f a b ∈ image2 f s t ↔ a ∈ s ∧ b ∈ t :=
  ⟨by
    rintro ⟨a', ha', b', hb', h⟩
    rcases hf h with ⟨rfl, rfl⟩
    exact ⟨ha', hb'⟩, fun ⟨ha, hb⟩ => mem_image2_of_mem ha hb⟩

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