le_iff_mem

Mathlib.Topology.Algebra.Algebra

URI: https://scilib.ai/kg/mathlib#Algebra.elemental.le_iff_mem

← MathLib Explorer

English

If hs is IsClosed(s as a set), then elemental R x ≤ s if and only if x ∈ s.

Русский

Пусть hs: IsClosed((s:Set A)). Тогда elemental R x ≤ s, если и только если x ∈ s.

LaTeX

$$IsClosed((s:Set A)) → (elemental R x ≤ s ↔ x ∈ s)$$

Lean4

theorem le_iff_mem {x : A} {s : Subalgebra R A} (hs : IsClosed (s : Set A)) : elemental R x ≤ s ↔ x ∈ s :=
  ⟨fun h ↦ h (self_mem R x), fun h ↦ le_of_mem hs h⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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