mem_inf — Mathlib

English

For any x in M, x belongs to the infimum N ⊓ N' iff x belongs to N and to N'.

Русский

Для любого x ∈ M верно: x ∈ N ⊓ N' тогда и только тогда, когда x ∈ N и x ∈ N'.

LaTeX

$$x \\in N \\cap N' \\\\iff \\\\ x \\in N \\land x \\in N'$$

Lean4

@[simp]
theorem mem_inf (x : M) : x ∈ N ⊓ N' ↔ x ∈ N ∧ x ∈ N' := by
  rw [← mem_toSubmodule, ← mem_toSubmodule, ← mem_toSubmodule, inf_toSubmodule, Submodule.mem_inf]

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