lt_iff — Mathlib

English

Extensionality for two-sided ideals: equality is determined by membership of every element.

Русский

Расширение для двусторонних идеалов: равенство определяется по членству каждого элемента.

LaTeX

$$I = J iff ∀ x, x ∈ I ↔ x ∈ J$$

Lean4

theorem lt_iff (I J : TwoSidedIdeal R) : I < J ↔ (I : Set R) ⊂ (J : Set R) :=
  by
  rw [lt_iff_le_and_ne, Set.ssubset_iff_subset_ne, le_iff]
  simp

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