lt_iff_le_and_exists

Mathlib.Data.SetLike.Basic

URI: https://scilib.ai/kg/mathlib#SetLike.lt_iff_le_and_exists

English

p < q if and only if p ≤ q and there exists x ∈ q with x ∉ p.

Русский

p < q эквивалентно p ≤ q и существует x ∈ q, такого что x ∉ p.

LaTeX

$$$ p < q \iff p \le q \land \exists x \in q, x \notin p $$$

Lean4

theorem lt_iff_le_and_exists : p < q ↔ p ≤ q ∧ ∃ x ∈ q, x ∉ p := by rw [lt_iff_le_not_ge, not_le_iff_exists]

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

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

Разделы

Аффилиация

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