sup_mem_iff

Mathlib.Order.Ideal

URI: https://scilib.ai/kg/mathlib#Order.Ideal.sup_mem_iff

English

If x ∈ s and y ∈ s, then x ⊔ y ∈ s.

Русский

Если x и y принадлежат s, то x ⊔ y принадлежит s.

LaTeX

$$x \in s \to y \in s \Rightarrow x \sqcup y \in s$$

Lean4

@[simp]
theorem sup_mem_iff : x ⊔ y ∈ I ↔ x ∈ I ∧ y ∈ I :=
  ⟨fun h ↦ ⟨I.lower le_sup_left h, I.lower le_sup_right h⟩, fun h ↦ sup_mem h.1 h.2⟩

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

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

Разделы

Аффилиация

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