ext — Mathlib

English

ValuationSubring K satisfies extensionality: two valuation subrings are equal if and only if they have the same elements.

Русский

ValuationSubring K удовлетворяет экстенсиональности: два валюационных подкольца равны тогда и только тогда, когда у них совпадают элементы.

LaTeX

$$$\forall A,B:\, (\forall x, x \in A \iff x \in B) \Rightarrow A = B$$$

Lean4

@[ext]
theorem ext (A B : ValuationSubring K) (h : ∀ x, x ∈ A ↔ x ∈ B) : A = B :=
  SetLike.ext h

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