mem_restrict' — Mathlib

English

Membership of J1 in π.restrict J is equivalent to existence of J' in π such that J1 equals J ∩ J'.

Русский

Принадлежность J1 к π.restrict J эквивалентна существованию J' в π, такому что J1 = J ∩ J'.

LaTeX

$$$ J_1 \\in π.restrict J \\iff \\exists J' \\in π, (J_1 : Set(ι \\rightarrow \\mathbb{R})) = ↑J \\cap ↑J' $$$

Lean4

theorem mem_restrict' : J₁ ∈ π.restrict J ↔ ∃ J' ∈ π, (J₁ : Set (ι → ℝ)) = ↑J ∩ ↑J' := by
  simp only [mem_restrict, ← Box.withBotCoe_inj, Box.coe_inf, Box.coe_coe]

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