mem_sInf — Mathlib

English

For a set S of subfields of K and element x ∈ K, x ∈ sInf S iff x ∈ p for all p ∈ S.

Русский

Для множества S подполья K и элемента x ∈ K: x ∈ sInf S тогда и только тогда, когда x ∈ p для всех p ∈ S.

LaTeX

$$$x \in sInf S \iff \forall p \in S,\; x \in p$$$

Lean4

theorem mem_sInf {S : Set (Subfield K)} {x : K} : x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p :=
  Subring.mem_sInf.trans ⟨fun h p hp => h p.toSubring ⟨p, hp, rfl⟩, fun h _ ⟨p', hp', p_eq⟩ => p_eq ▸ h p' hp'⟩

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