prod_sub_preimage_iff — Mathlib

English

Let W ⊆ γ and f : α × β → γ. Then s × t ⊆ f^{-1}(W) iff for all a ∈ s and b ∈ t, f(a,b) ∈ W.

Русский

Пусть W ⊆ γ и f : α × β → γ. Тогда s × t ⊆ f^{-1}(W) эквивалентно тому, что для всех a ∈ s и b ∈ t выполнено f(a,b) ∈ W.

LaTeX

$$$ s \times t \subseteq f^{-1}(W) \iff \forall a \in s, \forall b \in t, f(a,b) \in W $$$

Lean4

theorem prod_sub_preimage_iff {W : Set γ} {f : α × β → γ} : s ×ˢ t ⊆ f ⁻¹' W ↔ ∀ a b, a ∈ s → b ∈ t → f (a, b) ∈ W := by
  simp [subset_def]

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