mem_single — Mathlib

English

Let I be a box, J ≤ I a box, and J′ a box. The prepartition consisting of a single box J contains J′ if and only if J′ = J.

Русский

Пусть I — коробка, J ≤ I, и J′ — коробка. Предразбиение, состоящее из единственной коробки J, содержит J′ тогда и только тогда, когда J′ = J.

LaTeX

$$$J' \in \mathrm{single}(I,J,h) \iff J' = J$$$

Lean4

@[simp]
theorem mem_single {J'} (h : J ≤ I) : J' ∈ single I J h ↔ J' = J :=
  mem_singleton

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