mem_prod — Mathlib

English

For s ∈ Clopens α and t ∈ Clopens β, and x ∈ α × β, membership in s ×ˢ t is characterized by x.1 ∈ s and x.2 ∈ t.

Русский

Для клиноподмножеств s ∈ Clopens(α) и t ∈ Clopens(β) и элемента x ∈ α × β, принадлежность x в s ×ˢ t эквивалентна x₁ ∈ s и x₂ ∈ t.

LaTeX

$$$x \in s \timesˢ t \iff x.1 \in s \land x.2 \in t.$$$

Lean4

@[simp]
protected theorem mem_prod {s : Clopens α} {t : Clopens β} {x : α × β} : x ∈ s ×ˢ t ↔ x.1 ∈ s ∧ x.2 ∈ t :=
  .rfl

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