prod_coe — Mathlib

English

Membership in the product submodule p.prod q is equivalent to membership in p and q for the respective coordinates.

Русский

Принадлежность к произведению порожденного p.prod q эквивалентна принадлежности координатам x.fst ∈ p и x.snd ∈ q.

LaTeX

$$$$ x \\in p.prod q \\;\\iff\\; x_1 \\in p \\ \\wedge\\ x_2 \\in q $$$$

Lean4

@[simp]
theorem prod_coe : (prod p q₁ : Set (M × M')) = (p : Set M) ×ˢ (q₁ : Set M') :=
  rfl

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