inter_nonempty_iff_exists_left

Mathlib.Data.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.inter_nonempty_iff_exists_left

English

From (s ∩ t).Nonempty we can witness with x ∈ s and x ∈ t.

Русский

Из (s ∩ t).Nonempty следует существование x, такое что x ∈ s и x ∈ t.

LaTeX

$$$ (s \cap t).Nonempty \iff \exists x \in s, x \in t$$$

Lean4

theorem inter_nonempty_iff_exists_left : (s ∩ t).Nonempty ↔ ∃ x ∈ s, x ∈ t := by simp_rw [inter_nonempty]

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

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

Разделы

Аффилиация

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