mem_prod

Mathlib.Order.UpperLower.Prod

URI: https://scilib.ai/kg/mathlib#UpperSet.mem_prod

English

An element x ∈ α × β belongs to s ×ˢ t iff x.1 ∈ s and x.2 ∈ t.

Русский

Элемент x ∈ α × β принадлежит s ×ˢ t тогда и только тогда, когда x1 ∈ s и x2 ∈ t.

LaTeX

$$x ∈ s ×ˢ t ↔ x.1 ∈ s ∧ x.2 ∈ t$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru