We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 4c119ae commit d72d1eaCopy full SHA for d72d1ea
1 file changed
Mathlib/ModelTheory/PartialTypes.lean
@@ -139,6 +139,7 @@ def RealizedBy {M : Type w'} [L.Structure M] (p : T.PartialType α) (v : α →
139
∀ φ ∈ p, φ.Realize v
140
141
/-- A partial type is realized in a structure if some tuple realizes it. -/
142
+@[nolint unusedArguments]
143
def IsRealizedIn (p : T.PartialType α) (M : Type w') [L.Structure M] [M ⊨ T] [Nonempty M] :
144
Prop :=
145
∃ v : α → M, p.RealizedBy v
0 commit comments