leftRelDecidable — Mathlib

English

If membership in s is decidable, then the left coset relation on α is decidable.

Русский

Если членство в s разрешимо, то левое отношение косет разрешимо.

LaTeX

$$$\text{DecidablePred}(\cdot \in s) \Rightarrow \text{DecidableRel}((\text{leftRel } s).r)$$$

Lean4

@[to_additive]
instance leftRelDecidable [DecidablePred (· ∈ s)] : DecidableRel (leftRel s).r := fun x y =>
  by
  rw [leftRel_eq]
  exact ‹DecidablePred (· ∈ s)› _

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