mem_inf — Mathlib

English

For elements x ∈ E, membership in the infimum equals simultaneous membership in both fields: x ∈ S ∧ x ∈ T.

Русский

Для элемента x ∈ E принадлежность инфимума равна одновременному вхождению в оба поля: x ∈ S и x ∈ T.

LaTeX

$$$ x \\in S \\cap T \\iff x \\in S \\wedge x \\in T $$$

Lean4

@[simp]
theorem mem_inf {S T : IntermediateField F E} {x : E} : x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T :=
  Iff.rfl

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