Note about Mathlib/Init/
#
The files in Mathlib/Init
are leftovers from the port from Mathlib3.
(They contain content moved from lean3 itself that Mathlib needed but was not moved to lean4.)
We intend to move all the content of these files out into the main Mathlib
directory structure.
Contributions assisting with this are appreciated.
#align
statements without corresponding declarations
(i.e. because the declaration is in Batteries or Lean) can be left here.
These will be deleted soon so will not significantly delay deleting otherwise empty Init
files.
Equations
- instTransIff_mathlib = { trans := ⋯ }
Alias of the forward direction of not_not_not
.
Equations
- ExistsUnique p = ∃ (x : α), p x ∧ ∀ (y : α), p y → y = x
Instances For
Checks to see that xs
has only one binder.
Equations
- One or more equations did not get rendered due to their size.
Instances For
∃! x : α, p x
means that there exists a unique x
in α
such that p x
.
This is notation for ExistsUnique (fun (x : α) ↦ p x)
.
This notation does not allow multiple binders like ∃! (x : α) (y : β), p x y
as a shorthand for ∃! (x : α), ∃! (y : β), p x y
since it is liable to be misunderstood.
Often, the intended meaning is instead ∃! q : α × β, p q.1 q.2
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Pretty-printing for ExistsUnique
, following the same pattern as pretty printing for Exists
.
However, it does not merge binders.
Equations
- One or more equations did not get rendered due to their size.
Instances For
∃! x ∈ s, p x
means ∃! x, x ∈ s ∧ p x
, which is to say that there exists a unique x ∈ s
such that p x
.
Similarly, notations such as ∃! x ≤ n, p n
are supported,
using any relation defined using the binder_predicate
command.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Decidable.recOn_true p h₃ h₄ = cast ⋯ h₄
Instances For
Equations
- Decidable.recOn_false p h₃ h₄ = cast ⋯ h₄
Instances For
Alias of Decidable.byCases
.
Synonym for dite
(dependent if-then-else). We can construct an element q
(of any sort, not just a proposition) by cases on whether p
is true or false,
provided p
is decidable.
Equations
Instances For
Alias of Decidable.byContradiction
.
Equations
Instances For
A relation is transitive if x ≺ y
and y ≺ z
together imply x ≺ z
.
Equations
- Transitive r = ∀ ⦃x y z : β⦄, r x y → r y z → r x z
Instances For
A relation is antisymmetric if x ≺ y
and y ≺ x
together imply that x = y
.
Equations
- AntiSymmetric r = ∀ ⦃x y : β⦄, r x y → r y x → x = y
Instances For
Equations
- Commutative f = ∀ (a b : α), f a b = f b a
Instances For
Equations
- Associative f = ∀ (a b c : α), f (f a b) c = f a (f b c)
Instances For
Equations
- LeftIdentity f one = ∀ (a : α), f one a = a
Instances For
Equations
- RightIdentity f one = ∀ (a : α), f a one = a
Instances For
Equations
- RightInverse f inv one = ∀ (a : α), f a (inv a) = one
Instances For
Equations
- LeftCancelative f = ∀ (a b c : α), f a b = f a c → b = c
Instances For
Equations
- RightCancelative f = ∀ (a b c : α), f a b = f c b → a = c
Instances For
Equations
- LeftDistributive f g = ∀ (a b c : α), f a (g b c) = g (f a b) (f a c)
Instances For
Equations
- RightDistributive f g = ∀ (a b c : α), f (g a b) c = g (f a c) (f b c)
Instances For
Equations
- RightCommutative h = ∀ (b : β) (a₁ a₂ : α), h (h b a₁) a₂ = h (h b a₂) a₁
Instances For
Equations
- LeftCommutative h = ∀ (a₁ a₂ : α) (b : β), h a₁ (h a₂ b) = h a₂ (h a₁ b)