instSetLike — Mathlib

English

An intermediate field S is naturally regarded as a subset of L; in particular S is a set of elements of L.

Русский

Промежуточное поле S естественным образом рассматривается как подмножество L; в частности, S состоит из элементов L.

LaTeX

$$$S \subseteq L$ for every $S \in \operatorname{IntermediateField}(K,L)$$$

Lean4

instance : SetLike (IntermediateField K L) L :=
  ⟨fun S => S.toSubalgebra.carrier, by
    rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩
    simp⟩

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