Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+โ†‘Ctrl+โ†“to navigate, Ctrl+๐Ÿ–ฑ๏ธto focus. On Mac, use Cmdinstead of Ctrl.
/-
Copyright (c) 2018 Johannes Hรถlzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hรถlzl, Kenny Lau, Johan Commelin, Mario Carneiro, Kevin Buzzard,
Amelia Livingston, Yury Kudryashov, Yakov Pechersky

! This file was ported from Lean 3 source module group_theory.subsemigroup.basic
! leanprover-community/mathlib commit feb99064803fd3108e37c18b0f77d0a8344677a3
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Hom.Group
import Mathlib.Data.Set.Lattice
import Mathlib.Data.SetLike.Basic

/-!
# Subsemigroups: definition and `CompleteLattice` structure

This file defines bundled multiplicative and additive subsemigroups. We also define
a `CompleteLattice` structure on `Subsemigroup`s,
and define the closure of a set as the minimal subsemigroup that includes this set.

## Main definitions

* `Subsemigroup M`: the type of bundled subsemigroup of a magma `M`; the underlying set is given in
  the `carrier` field of the structure, and should be accessed through coercion as in `(S : Set M)`.
* `AddSubsemigroup M` : the type of bundled subsemigroups of an additive magma `M`.

For each of the following definitions in the `Subsemigroup` namespace, there is a corresponding
definition in the `AddSubsemigroup` namespace.

* `Subsemigroup.copy` : copy of a subsemigroup with `carrier` replaced by a set that is equal but
  possibly not definitionally equal to the carrier of the original `Subsemigroup`.
* `Subsemigroup.closure` :  semigroup closure of a set, i.e.,
  the least subsemigroup that includes the set.
* `Subsemigroup.gi` : `closure : Set M โ†’ Subsemigroup M` and coercion `coe : Subsemigroup M โ†’ Set M`
  form a `GaloisInsertion`;

## Implementation notes

Subsemigroup inclusion is denoted `โ‰ค` rather than `โŠ†`, although `โˆˆ` is defined as
membership of a subsemigroup's underlying set.

Note that `Subsemigroup M` does not actually require `Semigroup M`,
instead requiring only the weaker `Mul M`.

This file is designed to have very few dependencies. In particular, it should not use natural
numbers.

## Tags
subsemigroup, subsemigroups
-/


-- Only needed for notation
variable {
M: Type ?u.8983
M
:
Type _: Type (?u.4117+1)
Type _
} {
N: Type ?u.19092
N
:
Type _: Type (?u.29+1)
Type _
} {
A: Type ?u.5756
A
:
Type _: Type (?u.32+1)
Type _
} section NonAssoc variable [
Mul: Type ?u.19581 โ†’ Type ?u.19581
Mul
M: Type ?u.26
M
] {
s: Set M
s
:
Set: Type ?u.7487 โ†’ Type ?u.7487
Set
M: Type ?u.11
M
} variable [
Add: Type ?u.7490 โ†’ Type ?u.7490
Add
A: Type ?u.32
A
] {
t: Set A
t
:
Set: Type ?u.4857 โ†’ Type ?u.4857
Set
A: Type ?u.8989
A
} /-- `MulMemClass S M` says `S` is a type of sets `s : Set M` that are closed under `(*)` -/ class
MulMemClass: โˆ€ {S : Type u_1} {M : Type u_2} [inst : Mul M] [inst_1 : SetLike S M], (โˆ€ {s : S} {a b : M}, a โˆˆ s โ†’ b โˆˆ s โ†’ a * b โˆˆ s) โ†’ MulMemClass S M
MulMemClass
(
S: Type ?u.68
S
:
Type _: Type (?u.68+1)
Type _
) (
M: Type ?u.71
M
:
Type _: Type (?u.71+1)
Type _
) [
Mul: Type ?u.74 โ†’ Type ?u.74
Mul
M: Type ?u.71
M
] [
SetLike: Type ?u.78 โ†’ outParam (Type ?u.77) โ†’ Type (max?u.78?u.77)
SetLike
S: Type ?u.68
S
M: Type ?u.71
M
] :
Prop: Type
Prop
where /-- A substructure satisfying `MulMemClass` is closed under multiplication. -/
mul_mem: โˆ€ {S : Type u_1} {M : Type u_2} [inst : Mul M] [inst_1 : SetLike S M] [self : MulMemClass S M] {s : S} {a b : M}, a โˆˆ s โ†’ b โˆˆ s โ†’ a * b โˆˆ s
mul_mem
: โˆ€ {
s: S
s
:
S: Type ?u.68
S
} {
a: M
a
b: M
b
:
M: Type ?u.71
M
},
a: M
a
โˆˆ
s: S
s
โ†’
b: M
b
โˆˆ
s: S
s
โ†’
a: M
a
*
b: M
b
โˆˆ
s: S
s
#align mul_mem_class
MulMemClass: (S : Type u_1) โ†’ (M : Type u_2) โ†’ [inst : Mul M] โ†’ [inst : SetLike S M] โ†’ Prop
MulMemClass
export MulMemClass (mul_mem) /-- `AddMemClass S M` says `S` is a type of sets `s : Set M` that are closed under `(+)` -/ class
AddMemClass: (S : Type u_1) โ†’ (M : Type u_2) โ†’ [inst : Add M] โ†’ [inst : SetLike S M] โ†’ Prop
AddMemClass
(
S: Type ?u.251
S
:
Type _: Type (?u.251+1)
Type _
) (
M: Type ?u.254
M
:
Type _: Type (?u.254+1)
Type _
) [
Add: Type ?u.257 โ†’ Type ?u.257
Add
M: Type ?u.254
M
] [
SetLike: Type ?u.261 โ†’ outParam (Type ?u.260) โ†’ Type (max?u.261?u.260)
SetLike
S: Type ?u.251
S
M: Type ?u.254
M
] :
Prop: Type
Prop
where /-- A substructure satisfying `AddMemClass` is closed under addition. -/
add_mem: โˆ€ {S : Type u_1} {M : Type u_2} [inst : Add M] [inst_1 : SetLike S M] [self : AddMemClass S M] {s : S} {a b : M}, a โˆˆ s โ†’ b โˆˆ s โ†’ a + b โˆˆ s
add_mem
: โˆ€ {
s: S
s
:
S: Type ?u.251
S
} {
a: M
a
b: M
b
:
M: Type ?u.254
M
},
a: M
a
โˆˆ
s: S
s
โ†’
b: M
b
โˆˆ
s: S
s
โ†’
a: M
a
+
b: M
b
โˆˆ
s: S
s
#align add_mem_class
AddMemClass: (S : Type u_1) โ†’ (M : Type u_2) โ†’ [inst : Add M] โ†’ [inst : SetLike S M] โ†’ Prop
AddMemClass
export AddMemClass (add_mem) attribute [
to_additive: (S : Type u_1) โ†’ (M : Type u_2) โ†’ [inst : Add M] โ†’ [inst : SetLike S M] โ†’ Prop
to_additive
]
MulMemClass: (S : Type u_1) โ†’ (M : Type u_2) โ†’ [inst : Mul M] โ†’ [inst : SetLike S M] โ†’ Prop
MulMemClass
/-- A subsemigroup of a magma `M` is a subset closed under multiplication. -/ structure
Subsemigroup: (M : Type u_1) โ†’ [inst : Mul M] โ†’ Type u_1
Subsemigroup
(
M: Type ?u.436
M
:
Type _: Type (?u.436+1)
Type _
) [
Mul: Type ?u.439 โ†’ Type ?u.439
Mul
M: Type ?u.436
M
] where /-- The carrier of a subsemigroup. -/
carrier: {M : Type u_1} โ†’ [inst : Mul M] โ†’ Subsemigroup M โ†’ Set M
carrier
:
Set: Type ?u.444 โ†’ Type ?u.444
Set
M: Type ?u.436
M
/-- The product of two elements of a subsemigroup belongs to the subsemigroup. -/
mul_mem': โˆ€ {M : Type u_1} [inst : Mul M] (self : Subsemigroup M) {a b : M}, a โˆˆ self.carrier โ†’ b โˆˆ self.carrier โ†’ a * b โˆˆ self.carrier
mul_mem'
{
a: ?m.447
a
b: ?m.450
b
} :
a: ?m.447
a
โˆˆ
carrier: Set M
carrier
โ†’
b: ?m.450
b
โˆˆ
carrier: Set M
carrier
โ†’
a: ?m.447
a
*
b: ?m.450
b
โˆˆ
carrier: Set M
carrier
#align subsemigroup
Subsemigroup: (M : Type u_1) โ†’ [inst : Mul M] โ†’ Type u_1
Subsemigroup
/-- An additive subsemigroup of an additive magma `M` is a subset closed under addition. -/ structure
AddSubsemigroup: {M : Type u_1} โ†’ [inst : Add M] โ†’ (carrier : Set M) โ†’ (โˆ€ {a b : M}, a โˆˆ carrier โ†’ b โˆˆ carrier โ†’ a + b โˆˆ carrier) โ†’ AddSubsemigroup M
AddSubsemigroup
(
M: Type ?u.1006
M
:
Type _: Type (?u.1006+1)
Type _
) [
Add: Type ?u.1009 โ†’ Type ?u.1009
Add
M: Type ?u.1006
M
] where /-- The carrier of an additive subsemigroup. -/
carrier: {M : Type u_1} โ†’ [inst : Add M] โ†’ AddSubsemigroup M โ†’ Set M
carrier
:
Set: Type ?u.1014 โ†’ Type ?u.1014
Set
M: Type ?u.1006
M
/-- The sum of two elements of an additive subsemigroup belongs to the subsemigroup. -/
add_mem': โˆ€ {M : Type u_1} [inst : Add M] (self : AddSubsemigroup M) {a b : M}, a โˆˆ self.carrier โ†’ b โˆˆ self.carrier โ†’ a + b โˆˆ self.carrier
add_mem'
{
a: ?m.1017
a
b: ?m.1020
b
} :
a: ?m.1017
a
โˆˆ
carrier: Set M
carrier
โ†’
b: ?m.1020
b
โˆˆ
carrier: Set M
carrier
โ†’
a: ?m.1017
a
+
b: ?m.1020
b
โˆˆ
carrier: Set M
carrier
#align add_subsemigroup
AddSubsemigroup: (M : Type u_1) โ†’ [inst : Add M] โ†’ Type u_1
AddSubsemigroup
attribute [to_additive
AddSubsemigroup: (M : Type u_1) โ†’ [inst : Add M] โ†’ Type u_1
AddSubsemigroup
]
Subsemigroup: (M : Type u_1) โ†’ [inst : Mul M] โ†’ Type u_1
Subsemigroup
namespace Subsemigroup @[
to_additive: {M : Type u_1} โ†’ [inst : Add M] โ†’ SetLike (AddSubsemigroup M) M
to_additive
]
instance: {M : Type u_1} โ†’ [inst : Mul M] โ†’ SetLike (Subsemigroup M) M
instance
:
SetLike: Type ?u.1577 โ†’ outParam (Type ?u.1576) โ†’ Type (max?u.1577?u.1576)
SetLike
(
Subsemigroup: (M : Type ?u.1578) โ†’ [inst : Mul M] โ†’ Type ?u.1578
Subsemigroup
M: Type ?u.1555
M
)
M: Type ?u.1555
M
:= โŸจ
Subsemigroup.carrier: {M : Type ?u.1598} โ†’ [inst : Mul M] โ†’ Subsemigroup M โ†’ Set M
Subsemigroup.carrier
, fun
p: ?m.1620
p
q: ?m.1623
q
h: ?m.1626
h
=>

Goals accomplished! ๐Ÿ™
M: Type ?u.1555

N: Type ?u.1558

A: Type ?u.1561

instโœยน: Mul M

s: Set M

instโœ: Add A

t: Set A

p, q: Subsemigroup M

h: p.carrier = q.carrier


p = q
M: Type ?u.1555

N: Type ?u.1558

A: Type ?u.1561

instโœยน: Mul M

s: Set M

instโœ: Add A

t: Set A

q: Subsemigroup M

carrierโœ: Set M

mul_mem'โœ: โˆ€ {a b : M}, a โˆˆ carrierโœ โ†’ b โˆˆ carrierโœ โ†’ a * b โˆˆ carrierโœ

h: { carrier := carrierโœ, mul_mem' := mul_mem'โœ }.carrier = q.carrier


mk
{ carrier := carrierโœ, mul_mem' := mul_mem'โœ } = q
M: Type ?u.1555

N: Type ?u.1558

A: Type ?u.1561

instโœยน: Mul M

s: Set M

instโœ: Add A

t: Set A

q: Subsemigroup M

carrierโœ: Set M

mul_mem'โœ: โˆ€ {a b : M}, a โˆˆ carrierโœ โ†’ b โˆˆ carrierโœ โ†’ a * b โˆˆ carrierโœ

h: { carrier := carrierโœ, mul_mem' := mul_mem'โœ }.carrier = q.carrier


mk
{ carrier := carrierโœ, mul_mem' := mul_mem'โœ } = q
M: Type ?u.1555

N: Type ?u.1558

A: Type ?u.1561

instโœยน: Mul M

s: Set M

instโœ: Add A

t: Set A

p, q: Subsemigroup M

h: p.carrier = q.carrier


p = q
M: Type ?u.1555

N: Type ?u.1558

A: Type ?u.1561

instโœยน: Mul M

s: Set M

instโœ: Add A

t: Set A

carrierโœยน: Set M

mul_mem'โœยน: โˆ€ {a b : M}, a โˆˆ carrierโœยน โ†’ b โˆˆ carrierโœยน โ†’ a * b โˆˆ carrierโœยน

carrierโœ: Set M

mul_mem'โœ: โˆ€ {a b : M}, a โˆˆ carrierโœ โ†’ b โˆˆ carrierโœ โ†’ a * b โˆˆ carrierโœ

h: { carrier := carrierโœยน, mul_mem' := mul_mem'โœยน }.carrier = { carrier := carrierโœ, mul_mem' := mul_mem'โœ }.carrier


mk.mk
{ carrier := carrierโœยน, mul_mem' := mul_mem'โœยน } = { carrier := carrierโœ, mul_mem' := mul_mem'โœ }
M: Type ?u.1555

N: Type ?u.1558

A: Type ?u.1561

instโœยน: Mul M

s: Set M

instโœ: Add A

t: Set A

carrierโœยน: Set M

mul_mem'โœยน: โˆ€ {a b : M}, a โˆˆ carrierโœยน โ†’ b โˆˆ carrierโœยน โ†’ a * b โˆˆ carrierโœยน

carrierโœ: Set M

mul_mem'โœ: โˆ€ {a b : M}, a โˆˆ carrierโœ โ†’ b โˆˆ carrierโœ โ†’ a * b โˆˆ carrierโœ

h: { carrier := carrierโœยน, mul_mem' := mul_mem'โœยน }.carrier = { carrier := carrierโœ, mul_mem' := mul_mem'โœ }.carrier


mk.mk
{ carrier := carrierโœยน, mul_mem' := mul_mem'โœยน } = { carrier := carrierโœ, mul_mem' := mul_mem'โœ }
M: Type ?u.1555

N: Type ?u.1558

A: Type ?u.1561

instโœยน: Mul M

s: Set M

instโœ: Add A

t: Set A

p, q: Subsemigroup M

h: p.carrier = q.carrier


p = q

Goals accomplished! ๐Ÿ™
โŸฉ @[
to_additive: โˆ€ {M : Type u_1} [inst : Add M], AddMemClass (AddSubsemigroup M) M
to_additive
]
instance: โˆ€ {M : Type u_1} [inst : Mul M], MulMemClass (Subsemigroup M) M
instance
:
MulMemClass: (S : Type ?u.2144) โ†’ (M : Type ?u.2143) โ†’ [inst : Mul M] โ†’ [inst : SetLike S M] โ†’ Prop
MulMemClass
(
Subsemigroup: (M : Type ?u.2145) โ†’ [inst : Mul M] โ†’ Type ?u.2145
Subsemigroup
M: Type ?u.2122
M
)
M: Type ?u.2122
M
where mul_mem := fun {
_: ?m.2179
_
_: ?m.2182
_
_: ?m.2185
_
} =>
Subsemigroup.mul_mem': โˆ€ {M : Type ?u.2187} [inst : Mul M] (self : Subsemigroup M) {a b : M}, a โˆˆ self.carrier โ†’ b โˆˆ self.carrier โ†’ a * b โˆˆ self.carrier
Subsemigroup.mul_mem'
_: Subsemigroup ?m.2188
_
initialize_simps_projections
Subsemigroup: (M : Type u_1) โ†’ [inst : Mul M] โ†’ Type u_1
Subsemigroup
(
carrier: (M : Type u_1) โ†’ [inst : Mul M] โ†’ Subsemigroup M โ†’ Set M
carrier
โ†’
coe: (M : Type u_1) โ†’ [inst : Mul M] โ†’ Subsemigroup M โ†’ Set M
coe
) initialize_simps_projections
AddSubsemigroup: (M : Type u_1) โ†’ [inst : Add M] โ†’ Type u_1
AddSubsemigroup
(
carrier: (M : Type u_1) โ†’ [inst : Add M] โ†’ AddSubsemigroup M โ†’ Set M
carrier
โ†’
coe: (M : Type u_1) โ†’ [inst : Add M] โ†’ AddSubsemigroup M โ†’ Set M
coe
) @[
to_additive: โˆ€ {M : Type u_1} [inst : Add M] {s : AddSubsemigroup M} {x : M}, x โˆˆ s.carrier โ†” x โˆˆ s
to_additive
(attr := simp)] theorem
mem_carrier: โˆ€ {M : Type u_1} [inst : Mul M] {s : Subsemigroup M} {x : M}, x โˆˆ s.carrier โ†” x โˆˆ s
mem_carrier
{s :
Subsemigroup: (M : Type ?u.2374) โ†’ [inst : Mul M] โ†’ Type ?u.2374
Subsemigroup
M: Type ?u.2353
M
} {
x: M
x
:
M: Type ?u.2353
M
} :
x: M
x
โˆˆ s.
carrier: {M : Type ?u.2391} โ†’ [inst : Mul M] โ†’ Subsemigroup M โ†’ Set M
carrier
โ†”
x: M
x
โˆˆ s :=
Iff.rfl: โˆ€ {a : Prop}, a โ†” a
Iff.rfl
#align subsemigroup.mem_carrier
Subsemigroup.mem_carrier: โˆ€ {M : Type u_1} [inst : Mul M] {s : Subsemigroup M} {x : M}, x โˆˆ s.carrier โ†” x โˆˆ s
Subsemigroup.mem_carrier
#align add_subsemigroup.mem_carrier
AddSubsemigroup.mem_carrier: โˆ€ {M : Type u_1} [inst : Add M] {s : AddSubsemigroup M} {x : M}, x โˆˆ s.carrier โ†” x โˆˆ s
AddSubsemigroup.mem_carrier
@[
to_additive: โˆ€ {M : Type u_1} [inst : Add M] {s : Set M} {x : M} (h_mul : โˆ€ {a b : M}, a โˆˆ s โ†’ b โˆˆ s โ†’ a + b โˆˆ s), x โˆˆ { carrier := s, add_mem' := h_mul } โ†” x โˆˆ s
to_additive
(attr := simp)] theorem
mem_mk: โˆ€ {s : Set M} {x : M} (h_mul : โˆ€ {a b : M}, a โˆˆ s โ†’ b โˆˆ s โ†’ a * b โˆˆ s), x โˆˆ { carrier := s, mul_mem' := h_mul } โ†” x โˆˆ s
mem_mk
{
s: Set M
s
:
Set: Type ?u.2527 โ†’ Type ?u.2527
Set
M: Type ?u.2506
M
} {
x: M
x
:
M: Type ?u.2506
M
} (
h_mul: ?m.2532
h_mul
) :
x: M
x
โˆˆ
mk: {M : Type ?u.2540} โ†’ [inst : Mul M] โ†’ (carrier : Set M) โ†’ (โˆ€ {a b : M}, a โˆˆ carrier โ†’ b โˆˆ carrier โ†’ a * b โˆˆ carrier) โ†’ Subsemigroup M
mk
s: Set M
s
h_mul: ?m.2532
h_mul
โ†”
x: M
x
โˆˆ
s: Set M
s
:=
Iff.rfl: โˆ€ {a : Prop}, a โ†” a
Iff.rfl
#align subsemigroup.mem_mk
Subsemigroup.mem_mk: โˆ€ {M : Type u_1} [inst : Mul M] {s : Set M} {x : M} (h_mul : โˆ€ {a b : M}, a โˆˆ s โ†’ b โˆˆ s โ†’ a * b โˆˆ s), x โˆˆ { carrier := s, mul_mem' := h_mul } โ†” x โˆˆ s
Subsemigroup.mem_mk
#align add_subsemigroup.mem_mk
AddSubsemigroup.mem_mk: โˆ€ {M : Type u_1} [inst : Add M] {s : Set M} {x : M} (h_mul : โˆ€ {a b : M}, a โˆˆ s โ†’ b โˆˆ s โ†’ a + b โˆˆ s), x โˆˆ { carrier := s, add_mem' := h_mul } โ†” x โˆˆ s
AddSubsemigroup.mem_mk
@[
to_additive: โˆ€ {M : Type u_1} [inst : Add M] {s : Set M} (h_mul : โˆ€ {a b : M}, a โˆˆ s โ†’ b โˆˆ s โ†’ a + b โˆˆ s), โ†‘{ carrier := s, add_mem' := h_mul } = s
to_additive
(attr := simp)] theorem
coe_set_mk: โˆ€ {M : Type u_1} [inst : Mul M] {s : Set M} (h_mul : โˆ€ {a b : M}, a โˆˆ s โ†’ b โˆˆ s โ†’ a * b โˆˆ s), โ†‘{ carrier := s, mul_mem' := h_mul } = s
coe_set_mk
{
s: Set M
s
:
Set: Type ?u.2781 โ†’ Type ?u.2781
Set
M: Type ?u.2760
M
} (
h_mul: โˆ€ {a b : M}, a โˆˆ s โ†’ b โˆˆ s โ†’ a * b โˆˆ s
h_mul
) : (
mk: {M : Type ?u.2790} โ†’ [inst : Mul M] โ†’ (carrier : Set M) โ†’ (โˆ€ {a b : M}, a โˆˆ carrier โ†’ b โˆˆ carrier โ†’ a * b โˆˆ carrier) โ†’ Subsemigroup M
mk
s: Set M
s
h_mul: ?m.2784
h_mul
:
Set: Type ?u.2789 โ†’ Type ?u.2789
Set
M: Type ?u.2760
M
) =
s: Set M
s
:=
rfl: โˆ€ {ฮฑ : Sort ?u.2923} {a : ฮฑ}, a = a
rfl
#align subsemigroup.coe_set_mk
Subsemigroup.coe_set_mk: โˆ€ {M : Type u_1} [inst : Mul M] {s : Set M} (h_mul : โˆ€ {a b : M}, a โˆˆ s โ†’ b โˆˆ s โ†’ a * b โˆˆ s), โ†‘{ carrier := s, mul_mem' := h_mul } = s
Subsemigroup.coe_set_mk
#align add_subsemigroup.coe_set_mk
AddSubsemigroup.coe_set_mk: โˆ€ {M : Type u_1} [inst : Add M] {s : Set M} (h_mul : โˆ€ {a b : M}, a โˆˆ s โ†’ b โˆˆ s โ†’ a + b โˆˆ s), โ†‘{ carrier := s, add_mem' := h_mul } = s
AddSubsemigroup.coe_set_mk
@[
to_additive: โˆ€ {M : Type u_1} [inst : Add M] {s t : Set M} (h_mul : โˆ€ {a b : M}, a โˆˆ s โ†’ b โˆˆ s โ†’ a + b โˆˆ s) (h_mul' : โˆ€ {a b : M}, a โˆˆ t โ†’ b โˆˆ t โ†’ a + b โˆˆ t), { carrier := s, add_mem' := h_mul } โ‰ค { carrier := t, add_mem' := h_mul' } โ†” s โŠ† t
to_additive
(attr := simp)] theorem
mk_le_mk: โˆ€ {M : Type u_1} [inst : Mul M] {s t : Set M} (h_mul : โˆ€ {a b : M}, a โˆˆ s โ†’ b โˆˆ s โ†’ a * b โˆˆ s) (h_mul' : โˆ€ {a b : M}, a โˆˆ t โ†’ b โˆˆ t โ†’ a * b โˆˆ t), { carrier := s, mul_mem' := h_mul } โ‰ค { carrier := t, mul_mem' := h_mul' } โ†” s โŠ† t
mk_le_mk
{
s: Set M
s
t: Set M
t
:
Set: Type ?u.3065 โ†’ Type ?u.3065
Set
M: Type ?u.3041
M
} (
h_mul: โˆ€ {a b : M}, a โˆˆ s โ†’ b โˆˆ s โ†’ a * b โˆˆ s
h_mul
) (
h_mul': โˆ€ {a b : M}, a โˆˆ t โ†’ b โˆˆ t โ†’ a * b โˆˆ t
h_mul'
) :
mk: {M : Type ?u.3075} โ†’ [inst : Mul M] โ†’ (carrier : Set M) โ†’ (โˆ€ {a b : M}, a โˆˆ carrier โ†’ b โˆˆ carrier โ†’ a * b โˆˆ carrier) โ†’ Subsemigroup M
mk
s: Set M
s
h_mul: ?m.3068
h_mul
โ‰ค
mk: {M : Type ?u.3088} โ†’ [inst : Mul M] โ†’ (carrier : Set M) โ†’ (โˆ€ {a b : M}, a โˆˆ carrier โ†’ b โˆˆ carrier โ†’ a * b โˆˆ carrier) โ†’ Subsemigroup M
mk
t: Set M
t
h_mul': ?m.3071
h_mul'
โ†”
s: Set M
s
โŠ†
t: Set M
t
:=
Iff.rfl: โˆ€ {a : Prop}, a โ†” a
Iff.rfl
#align subsemigroup.mk_le_mk
Subsemigroup.mk_le_mk: โˆ€ {M : Type u_1} [inst : Mul M] {s t : Set M} (h_mul : โˆ€ {a b : M}, a โˆˆ s โ†’ b โˆˆ s โ†’ a * b โˆˆ s) (h_mul' : โˆ€ {a b : M}, a โˆˆ t โ†’ b โˆˆ t โ†’ a * b โˆˆ t), { carrier := s, mul_mem' := h_mul } โ‰ค { carrier := t, mul_mem' := h_mul' } โ†” s โŠ† t
Subsemigroup.mk_le_mk
#align add_subsemigroup.mk_le_mk
AddSubsemigroup.mk_le_mk: โˆ€ {M : Type u_1} [inst : Add M] {s t : Set M} (h_mul : โˆ€ {a b : M}, a โˆˆ s โ†’ b โˆˆ s โ†’ a + b โˆˆ s) (h_mul' : โˆ€ {a b : M}, a โˆˆ t โ†’ b โˆˆ t โ†’ a + b โˆˆ t), { carrier := s, add_mem' := h_mul } โ‰ค { carrier := t, add_mem' := h_mul' } โ†” s โŠ† t
AddSubsemigroup.mk_le_mk
/-- Two subsemigroups are equal if they have the same elements. -/ @[
to_additive: โˆ€ {M : Type u_1} [inst : Add M] {S T : AddSubsemigroup M}, (โˆ€ (x : M), x โˆˆ S โ†” x โˆˆ T) โ†’ S = T
to_additive
(attr := ext) "Two `AddSubsemigroup`s are equal if they have the same elements."] theorem
ext: โˆ€ {M : Type u_1} [inst : Mul M] {S T : Subsemigroup M}, (โˆ€ (x : M), x โˆˆ S โ†” x โˆˆ T) โ†’ S = T
ext
{S T :
Subsemigroup: (M : Type ?u.3536) โ†’ [inst : Mul M] โ†’ Type ?u.3536
Subsemigroup
M: Type ?u.3505
M
} (
h: โˆ€ (x : M), x โˆˆ S โ†” x โˆˆ T
h
: โˆ€
x: ?m.3541
x
,
x: ?m.3541
x
โˆˆ S โ†”
x: ?m.3541
x
โˆˆ T) : S = T :=
SetLike.ext: โˆ€ {A : Type ?u.3604} {B : Type ?u.3603} [i : SetLike A B] {p q : A}, (โˆ€ (x : B), x โˆˆ p โ†” x โˆˆ q) โ†’ p = q
SetLike.ext
h: โˆ€ (x : M), x โˆˆ S โ†” x โˆˆ T
h
#align subsemigroup.ext
Subsemigroup.ext: โˆ€ {M : Type u_1} [inst : Mul M] {S T : Subsemigroup M}, (โˆ€ (x : M), x โˆˆ S โ†” x โˆˆ T) โ†’ S = T
Subsemigroup.ext
#align add_subsemigroup.ext
AddSubsemigroup.ext: โˆ€ {M : Type u_1} [inst : Add M] {S T : AddSubsemigroup M}, (โˆ€ (x : M), x โˆˆ S โ†” x โˆˆ T) โ†’ S = T
AddSubsemigroup.ext
/-- Copy a subsemigroup replacing `carrier` with a set that is equal to it. -/ @[
to_additive: {M : Type u_1} โ†’ [inst : Add M] โ†’ (S : AddSubsemigroup M) โ†’ (s : Set M) โ†’ s = โ†‘S โ†’ AddSubsemigroup M
to_additive
"Copy an additive subsemigroup replacing `carrier` with a set that is equal to it."] protected def
copy: (S : Subsemigroup M) โ†’ (s : Set M) โ†’ s = โ†‘S โ†’ Subsemigroup M
copy
(S :
Subsemigroup: (M : Type ?u.3712) โ†’ [inst : Mul M] โ†’ Type ?u.3712
Subsemigroup
M: Type ?u.3691
M
) (
s: Set M
s
:
Set: Type ?u.3722 โ†’ Type ?u.3722
Set
M: Type ?u.3691
M
) (
hs: s = โ†‘S
hs
:
s: Set M
s
= S) :
Subsemigroup: (M : Type ?u.3885) โ†’ [inst : Mul M] โ†’ Type ?u.3885
Subsemigroup
M: Type ?u.3691
M
where carrier :=
s: Set M
s
mul_mem' :=
hs: s = โ†‘S
hs
.
symm: โˆ€ {ฮฑ : Sort ?u.3898} {a b : ฮฑ}, a = b โ†’ b = a
symm
โ–ธ S.
mul_mem': โˆ€ {M : Type ?u.3909} [inst : Mul M] (self : Subsemigroup M) {a b : M}, a โˆˆ self.carrier โ†’ b โˆˆ self.carrier โ†’ a * b โˆˆ self.carrier
mul_mem'
#align subsemigroup.copy
Subsemigroup.copy: {M : Type u_1} โ†’ [inst : Mul M] โ†’ (S : Subsemigroup M) โ†’ (s : Set M) โ†’ s = โ†‘S โ†’ Subsemigroup M
Subsemigroup.copy
#align add_subsemigroup.copy
AddSubsemigroup.copy: {M : Type u_1} โ†’ [inst : Add M] โ†’ (S : AddSubsemigroup M) โ†’ (s : Set M) โ†’ s = โ†‘S โ†’ AddSubsemigroup M
AddSubsemigroup.copy
variable {S :
Subsemigroup: (M : Type ?u.12567) โ†’ [inst : Mul M] โ†’ Type ?u.12567
Subsemigroup
M: Type ?u.4117
M
} @[
to_additive: โˆ€ {M : Type u_1} [inst : Add M] {S : AddSubsemigroup M} {s : Set M} (hs : s = โ†‘S), โ†‘(AddSubsemigroup.copy S s hs) = s
to_additive
(attr := simp)] theorem
coe_copy: โˆ€ {s : Set M} (hs : s = โ†‘S), โ†‘(Subsemigroup.copy S s hs) = s
coe_copy
{
s: Set M
s
:
Set: Type ?u.4179 โ†’ Type ?u.4179
Set
M: Type ?u.4148
M
} (
hs: s = โ†‘S
hs
:
s: Set M
s
= S) : (S.
copy: {M : Type ?u.4346} โ†’ [inst : Mul M] โ†’ (S : Subsemigroup M) โ†’ (s : Set M) โ†’ s = โ†‘S โ†’ Subsemigroup M
copy
s: Set M
s
hs: s = โ†‘S
hs
:
Set: Type ?u.4345 โ†’ Type ?u.4345
Set
M: Type ?u.4148
M
) =
s: Set M
s
:=
rfl: โˆ€ {ฮฑ : Sort ?u.4437} {a : ฮฑ}, a = a
rfl
#align subsemigroup.coe_copy
Subsemigroup.coe_copy: โˆ€ {M : Type u_1} [inst : Mul M] {S : Subsemigroup M} {s : Set M} (hs : s = โ†‘S), โ†‘(Subsemigroup.copy S s hs) = s
Subsemigroup.coe_copy
#align add_subsemigroup.coe_copy
AddSubsemigroup.coe_copy: โˆ€ {M : Type u_1} [inst : Add M] {S : AddSubsemigroup M} {s : Set M} (hs : s = โ†‘S), โ†‘(AddSubsemigroup.copy S s hs) = s
AddSubsemigroup.coe_copy
@[
to_additive: โˆ€ {M : Type u_1} [inst : Add M] {S : AddSubsemigroup M} {s : Set M} (hs : s = โ†‘S), AddSubsemigroup.copy S s hs = S
to_additive
] theorem
copy_eq: โˆ€ {s : Set M} (hs : s = โ†‘S), Subsemigroup.copy S s hs = S
copy_eq
{
s: Set M
s
:
Set: Type ?u.4545 โ†’ Type ?u.4545
Set
M: Type ?u.4514
M
} (
hs: s = โ†‘S
hs
:
s: Set M
s
= S) : S.
copy: {M : Type ?u.4710} โ†’ [inst : Mul M] โ†’ (S : Subsemigroup M) โ†’ (s : Set M) โ†’ s = โ†‘S โ†’ Subsemigroup M
copy
s: Set M
s
hs: s = โ†‘S
hs
= S :=
SetLike.coe_injective: โˆ€ {A : Type ?u.4732} {B : Type ?u.4733} [i : SetLike A B], Function.Injective SetLike.coe
SetLike.coe_injective
hs: s = โ†‘S
hs
#align subsemigroup.copy_eq
Subsemigroup.copy_eq: โˆ€ {M : Type u_1} [inst : Mul M] {S : Subsemigroup M} {s : Set M} (hs : s = โ†‘S), Subsemigroup.copy S s hs = S
Subsemigroup.copy_eq
#align add_subsemigroup.copy_eq
AddSubsemigroup.copy_eq: โˆ€ {M : Type u_1} [inst : Add M] {S : AddSubsemigroup M} {s : Set M} (hs : s = โ†‘S), AddSubsemigroup.copy S s hs = S
AddSubsemigroup.copy_eq
variable (
S: ?m.4836
S
) /-- A subsemigroup is closed under multiplication. -/ @[
to_additive: โˆ€ {M : Type u_1} [inst : Add M] (S : AddSubsemigroup M) {x y : M}, x โˆˆ S โ†’ y โˆˆ S โ†’ x + y โˆˆ S
to_additive
"An `AddSubsemigroup` is closed under addition."] protected theorem
mul_mem: โˆ€ {x y : M}, x โˆˆ S โ†’ y โˆˆ S โ†’ x * y โˆˆ S
mul_mem
{
x: M
x
y: M
y
:
M: Type ?u.4839
M
} :
x: M
x
โˆˆ S โ†’
y: M
y
โˆˆ S โ†’
x: M
x
*
y: M
y
โˆˆ S :=
Subsemigroup.mul_mem': โˆ€ {M : Type ?u.4999} [inst : Mul M] (self : Subsemigroup M) {a b : M}, a โˆˆ self.carrier โ†’ b โˆˆ self.carrier โ†’ a * b โˆˆ self.carrier
Subsemigroup.mul_mem'
S #align subsemigroup.mul_mem
Subsemigroup.mul_mem: โˆ€ {M : Type u_1} [inst : Mul M] (S : Subsemigroup M) {x y : M}, x โˆˆ S โ†’ y โˆˆ S โ†’ x * y โˆˆ S
Subsemigroup.mul_mem
#align add_subsemigroup.add_mem
AddSubsemigroup.add_mem: โˆ€ {M : Type u_1} [inst : Add M] (S : AddSubsemigroup M) {x y : M}, x โˆˆ S โ†’ y โˆˆ S โ†’ x + y โˆˆ S
AddSubsemigroup.add_mem
/-- The subsemigroup `M` of the magma `M`. -/ @[
to_additive: {M : Type u_1} โ†’ [inst : Add M] โ†’ Top (AddSubsemigroup M)
to_additive
"The additive subsemigroup `M` of the magma `M`."]
instance: {M : Type u_1} โ†’ [inst : Mul M] โ†’ Top (Subsemigroup M)
instance
:
Top: Type ?u.5090 โ†’ Type ?u.5090
Top
(
Subsemigroup: (M : Type ?u.5091) โ†’ [inst : Mul M] โ†’ Type ?u.5091
Subsemigroup
M: Type ?u.5059
M
) := โŸจ{ carrier :=
Set.univ: {ฮฑ : Type ?u.5110} โ†’ Set ฮฑ
Set.univ
mul_mem' := fun
_: ?m.5117
_
_: ?m.5120
_
=>
Set.mem_univ: โˆ€ {ฮฑ : Type ?u.5122} (x : ฮฑ), x โˆˆ Set.univ
Set.mem_univ
_: ?m.5123
_
}โŸฉ /-- The trivial subsemigroup `โˆ…` of a magma `M`. -/ @[
to_additive: {M : Type u_1} โ†’ [inst : Add M] โ†’ Bot (AddSubsemigroup M)
to_additive
"The trivial `AddSubsemigroup` `โˆ…` of an additive magma `M`."]
instance: {M : Type u_1} โ†’ [inst : Mul M] โ†’ Bot (Subsemigroup M)
instance
:
Bot: Type ?u.5278 โ†’ Type ?u.5278
Bot
(
Subsemigroup: (M : Type ?u.5279) โ†’ [inst : Mul M] โ†’ Type ?u.5279
Subsemigroup
M: Type ?u.5247
M
) := โŸจ{ carrier :=
โˆ…: ?m.5299
โˆ…
mul_mem' :=
False.elim: โˆ€ {C : Sort ?u.5344}, False โ†’ C
False.elim
}โŸฉ @[
to_additive: {M : Type u_1} โ†’ [inst : Add M] โ†’ Inhabited (AddSubsemigroup M)
to_additive
]
instance: {M : Type u_1} โ†’ [inst : Mul M] โ†’ Inhabited (Subsemigroup M)
instance
:
Inhabited: Sort ?u.5485 โ†’ Sort (max1?u.5485)
Inhabited
(
Subsemigroup: (M : Type ?u.5486) โ†’ [inst : Mul M] โ†’ Type ?u.5486
Subsemigroup
M: Type ?u.5454
M
) := โŸจ
โŠฅ: ?m.5501
โŠฅ
โŸฉ @[
to_additive: โˆ€ {M : Type u_1} [inst : Add M] {x : M}, ยฌx โˆˆ โŠฅ
to_additive
] theorem
not_mem_bot: โˆ€ {M : Type u_1} [inst : Mul M] {x : M}, ยฌx โˆˆ โŠฅ
not_mem_bot
{
x: M
x
:
M: Type ?u.5615
M
} :
x: M
x
โˆ‰ (
โŠฅ: ?m.5663
โŠฅ
:
Subsemigroup: (M : Type ?u.5654) โ†’ [inst : Mul M] โ†’ Type ?u.5654
Subsemigroup
M: Type ?u.5615
M
) :=
Set.not_mem_empty: โˆ€ {ฮฑ : Type ?u.5723} (x : ฮฑ), ยฌx โˆˆ โˆ…
Set.not_mem_empty
x: M
x
#align subsemigroup.not_mem_bot
Subsemigroup.not_mem_bot: โˆ€ {M : Type u_1} [inst : Mul M] {x : M}, ยฌx โˆˆ โŠฅ
Subsemigroup.not_mem_bot
#align add_subsemigroup.not_mem_bot
AddSubsemigroup.not_mem_bot: โˆ€ {M : Type u_1} [inst : Add M] {x : M}, ยฌx โˆˆ โŠฅ
AddSubsemigroup.not_mem_bot
@[
to_additive: โˆ€ {M : Type u_1} [inst : Add M] (x : M), x โˆˆ โŠค
to_additive
(attr := simp)] theorem
mem_top: โˆ€ (x : M), x โˆˆ โŠค
mem_top
(
x: M
x
:
M: Type ?u.5750
M
) :
x: M
x
โˆˆ (
โŠค: ?m.5810
โŠค
:
Subsemigroup: (M : Type ?u.5801) โ†’ [inst : Mul M] โ†’ Type ?u.5801
Subsemigroup
M: Type ?u.5750
M
) :=
Set.mem_univ: โˆ€ {ฮฑ : Type ?u.5865} (x : ฮฑ), x โˆˆ Set.univ
Set.mem_univ
x: M
x
#align subsemigroup.mem_top
Subsemigroup.mem_top: โˆ€ {M : Type u_1} [inst : Mul M] (x : M), x โˆˆ โŠค
Subsemigroup.mem_top
#align add_subsemigroup.mem_top
AddSubsemigroup.mem_top: โˆ€ {M : Type u_1} [inst : Add M] (x : M), x โˆˆ โŠค
AddSubsemigroup.mem_top
@[
to_additive: โˆ€ {M : Type u_1} [inst : Add M], โ†‘โŠค = Set.univ
to_additive
(attr := simp)] theorem
coe_top: โ†‘โŠค = Set.univ
coe_top
: ((
โŠค: ?m.5971
โŠค
:
Subsemigroup: (M : Type ?u.5962) โ†’ [inst : Mul M] โ†’ Type ?u.5962
Subsemigroup
M: Type ?u.5927
M
) :
Set: Type ?u.5960 โ†’ Type ?u.5960
Set
M: Type ?u.5927
M
) =
Set.univ: {ฮฑ : Type ?u.6091} โ†’ Set ฮฑ
Set.univ
:=
rfl: โˆ€ {ฮฑ : Sort ?u.6123} {a : ฮฑ}, a = a
rfl
#align subsemigroup.coe_top
Subsemigroup.coe_top: โˆ€ {M : Type u_1} [inst : Mul M], โ†‘โŠค = Set.univ
Subsemigroup.coe_top
#align add_subsemigroup.coe_top
AddSubsemigroup.coe_top: โˆ€ {M : Type u_1} [inst : Add M], โ†‘โŠค = Set.univ
AddSubsemigroup.coe_top
@[
to_additive: โˆ€ {M : Type u_1} [inst : Add M], โ†‘โŠฅ = โˆ…
to_additive
(attr := simp)] theorem
coe_bot: โˆ€ {M : Type u_1} [inst : Mul M], โ†‘โŠฅ = โˆ…
coe_bot
: ((
โŠฅ: ?m.6210
โŠฅ
:
Subsemigroup: (M : Type ?u.6201) โ†’ [inst : Mul M] โ†’ Type ?u.6201
Subsemigroup
M: Type ?u.6166
M
) :
Set: Type ?u.6199 โ†’ Type ?u.6199
Set
M: Type ?u.6166
M
) =
โˆ…: ?m.6336
โˆ…
:=
rfl: โˆ€ {ฮฑ : Sort ?u.6412} {a : ฮฑ}, a = a
rfl
#align subsemigroup.coe_bot
Subsemigroup.coe_bot: โˆ€ {M : Type u_1} [inst : Mul M], โ†‘โŠฅ = โˆ…
Subsemigroup.coe_bot
#align add_subsemigroup.coe_bot
AddSubsemigroup.coe_bot: โˆ€ {M : Type u_1} [inst : Add M], โ†‘โŠฅ = โˆ…
AddSubsemigroup.coe_bot
/-- The inf of two subsemigroups is their intersection. -/ @[
to_additive: {M : Type u_1} โ†’ [inst : Add M] โ†’ Inf (AddSubsemigroup M)
to_additive
"The inf of two `AddSubsemigroup`s is their intersection."]
instance: {M : Type u_1} โ†’ [inst : Mul M] โ†’ Inf (Subsemigroup M)
instance
:
Inf: Type ?u.6486 โ†’ Type ?u.6486
Inf
(
Subsemigroup: (M : Type ?u.6487) โ†’ [inst : Mul M] โ†’ Type ?u.6487
Subsemigroup
M: Type ?u.6455
M
) := โŸจfun
Sโ‚: ?m.6502
Sโ‚
Sโ‚‚: ?m.6505
Sโ‚‚
=> { carrier :=
Sโ‚: ?m.6502
Sโ‚
โˆฉ
Sโ‚‚: ?m.6505
Sโ‚‚
mul_mem' := fun โŸจ
hx: aโœ โˆˆ โ†‘Sโ‚
hx
,
hx': aโœ โˆˆ โ†‘Sโ‚‚
hx'
โŸฉ โŸจ
hy: bโœ โˆˆ โ†‘Sโ‚
hy
,
hy': bโœ โˆˆ โ†‘Sโ‚‚
hy'
โŸฉ => โŸจ
Sโ‚: ?m.6502
Sโ‚
.
mul_mem: โˆ€ {M : Type ?u.6734} [inst : Mul M] (S : Subsemigroup M) {x y : M}, x โˆˆ S โ†’ y โˆˆ S โ†’ x * y โˆˆ S
mul_mem
hx: aโœ โˆˆ โ†‘Sโ‚
hx
hy: bโœ โˆˆ โ†‘Sโ‚
hy
,
Sโ‚‚: ?m.6505
Sโ‚‚
.
mul_mem: โˆ€ {M : Type ?u.6761} [inst : Mul M] (S : Subsemigroup M) {x y : M}, x โˆˆ S โ†’ y โˆˆ S โ†’ x * y โˆˆ S
mul_mem
hx': aโœ โˆˆ โ†‘Sโ‚‚
hx'
hy': bโœ โˆˆ โ†‘Sโ‚‚
hy'
โŸฉ }โŸฉ @[
to_additive: โˆ€ {M : Type u_1} [inst : Add M] (p p' : AddSubsemigroup M), โ†‘(p โŠ“ p') = โ†‘p โˆฉ โ†‘p'
to_additive
(attr := simp)] theorem
coe_inf: โˆ€ (p p' : Subsemigroup M), โ†‘(p โŠ“ p') = โ†‘p โˆฉ โ†‘p'
coe_inf
(p p' :
Subsemigroup: (M : Type ?u.7142) โ†’ [inst : Mul M] โ†’ Type ?u.7142
Subsemigroup
M: Type ?u.7101
M
) : ((p โŠ“ p' :
Subsemigroup: (M : Type ?u.7150) โ†’ [inst : Mul M] โ†’ Type ?u.7150
Subsemigroup
M: Type ?u.7101
M
) :
Set: Type ?u.7148 โ†’ Type ?u.7148
Set
M: Type ?u.7101
M
) = (p :
Set: Type ?u.7275 โ†’ Type ?u.7275
Set
M: Type ?u.7101
M
) โˆฉ p' :=
rfl: โˆ€ {ฮฑ : Sort ?u.7410} {a : ฮฑ}, a = a
rfl
#align subsemigroup.coe_inf
Subsemigroup.coe_inf: โˆ€ {M : Type u_1} [inst : Mul M] (p p' : Subsemigroup M), โ†‘(p โŠ“ p') = โ†‘p โˆฉ โ†‘p'
Subsemigroup.coe_inf
#align add_subsemigroup.coe_inf
AddSubsemigroup.coe_inf: โˆ€ {M : Type u_1} [inst : Add M] (p p' : AddSubsemigroup M), โ†‘(p โŠ“ p') = โ†‘p โˆฉ โ†‘p'
AddSubsemigroup.coe_inf
@[
to_additive: โˆ€ {M : Type u_1} [inst : Add M] {p p' : AddSubsemigroup M} {x : M}, x โˆˆ p โŠ“ p' โ†” x โˆˆ p โˆง x โˆˆ p'
to_additive
(attr := simp)] theorem
mem_inf: โˆ€ {p p' : Subsemigroup M} {x : M}, x โˆˆ p โŠ“ p' โ†” x โˆˆ p โˆง x โˆˆ p'
mem_inf
{p p' :
Subsemigroup: (M : Type ?u.7516) โ†’ [inst : Mul M] โ†’ Type ?u.7516
Subsemigroup
M: Type ?u.7475
M
} {
x: M
x
:
M: Type ?u.7475
M
} :
x: M
x
โˆˆ p โŠ“ p' โ†”
x: M
x
โˆˆ p โˆง
x: M
x
โˆˆ p' :=
Iff.rfl: โˆ€ {a : Prop}, a โ†” a
Iff.rfl
#align subsemigroup.mem_inf
Subsemigroup.mem_inf: โˆ€ {M : Type u_1} [inst : Mul M] {p p' : Subsemigroup M} {x : M}, x โˆˆ p โŠ“ p' โ†” x โˆˆ p โˆง x โˆˆ p'
Subsemigroup.mem_inf
#align add_subsemigroup.mem_inf
AddSubsemigroup.mem_inf: โˆ€ {M : Type u_1} [inst : Add M] {p p' : AddSubsemigroup M} {x : M}, x โˆˆ p โŠ“ p' โ†” x โˆˆ p โˆง x โˆˆ p'
AddSubsemigroup.mem_inf
@[
to_additive: {M : Type u_1} โ†’ [inst : Add M] โ†’ InfSet (AddSubsemigroup M)
to_additive
]
instance: {M : Type u_1} โ†’ [inst : Mul M] โ†’ InfSet (Subsemigroup M)
instance
:
InfSet: Type ?u.7712 โ†’ Type ?u.7712
InfSet
(
Subsemigroup: (M : Type ?u.7713) โ†’ [inst : Mul M] โ†’ Type ?u.7713
Subsemigroup
M: Type ?u.7681
M
) := โŸจfun
s: ?m.7728
s
=> { carrier := โ‹‚
t: ?m.7742
t
โˆˆ
s: ?m.7728
s
, โ†‘
t: ?m.7742
t
mul_mem' := fun
hx: ?m.7878
hx
hy: ?m.7881
hy
=>
Set.mem_biInter: โˆ€ {ฮฑ : Type ?u.7883} {ฮฒ : Type ?u.7884} {s : Set ฮฑ} {t : ฮฑ โ†’ Set ฮฒ} {y : ฮฒ}, (โˆ€ (x : ฮฑ), x โˆˆ s โ†’ y โˆˆ t x) โ†’ y โˆˆ Set.iInter fun x => Set.iInter fun h => t x
Set.mem_biInter
fun
i: ?m.7915
i
h: ?m.7918
h
=>
i: ?m.7915
i
.
mul_mem: โˆ€ {M : Type ?u.7920} [inst : Mul M] (S : Subsemigroup M) {x y : M}, x โˆˆ S โ†’ y โˆˆ S โ†’ x * y โˆˆ S
mul_mem
(

Goals accomplished! ๐Ÿ™
M: Type ?u.7681

N: Type ?u.7684

A: Type ?u.7687

instโœยน: Mul M

sโœ: Set M

instโœ: Add A

t: Set A

S: Subsemigroup M

s: Set (Subsemigroup M)

aโœ, bโœ: M

hx: aโœ โˆˆ Set.iInter fun t => Set.iInter fun h => โ†‘t

hy: bโœ โˆˆ Set.iInter fun t => Set.iInter fun h => โ†‘t

i: Subsemigroup M

h: i โˆˆ s


aโœ โˆˆ i

Goals accomplished! ๐Ÿ™
) (

Goals accomplished! ๐Ÿ™
M: Type ?u.7681

N: Type ?u.7684

A: Type ?u.7687

instโœยน: Mul M

sโœ: Set M

instโœ: Add A

t: Set A

S: Subsemigroup M

s: Set (Subsemigroup M)

aโœ, bโœ: M

hx: aโœ โˆˆ Set.iInter fun t => Set.iInter fun h => โ†‘t

hy: bโœ โˆˆ Set.iInter fun t => Set.iInter fun h => โ†‘t

i: Subsemigroup M

h: i โˆˆ s


bโœ โˆˆ i

Goals accomplished! ๐Ÿ™
) }โŸฉ @[
to_additive: โˆ€ {M : Type u_1} [inst : Add M] (S : Set (AddSubsemigroup M)), โ†‘(sInf S) = Set.iInter fun s => Set.iInter fun h => โ†‘s
to_additive
(attr := simp, norm_cast)] theorem
coe_sInf: โˆ€ (S : Set (Subsemigroup M)), โ†‘(sInf S) = Set.iInter fun s => Set.iInter fun h => โ†‘s
coe_sInf
(S :
Set: Type ?u.8245 โ†’ Type ?u.8245
Set
(
Subsemigroup: (M : Type ?u.8246) โ†’ [inst : Mul M] โ†’ Type ?u.8246
Subsemigroup
M: Type ?u.8214
M
)) : ((
sInf: {ฮฑ : Type ?u.8262} โ†’ [self : InfSet ฮฑ] โ†’ Set ฮฑ โ†’ ฮฑ
sInf
S :
Subsemigroup: (M : Type ?u.8260) โ†’ [inst : Mul M] โ†’ Type ?u.8260
Subsemigroup
M: Type ?u.8214
M
) :
Set: Type ?u.8258 โ†’ Type ?u.8258
Set
M: Type ?u.8214
M
) = โ‹‚
s: ?m.8386
s
โˆˆ S, โ†‘
s: ?m.8386
s
:=
rfl: โˆ€ {ฮฑ : Sort ?u.8668} {a : ฮฑ}, a = a
rfl
#align subsemigroup.coe_Inf
Subsemigroup.coe_sInf: โˆ€ {M : Type u_1} [inst : Mul M] (S : Set (Subsemigroup M)), โ†‘(sInf S) = Set.iInter fun s => Set.iInter fun h => โ†‘s
Subsemigroup.coe_sInf
#align add_subsemigroup.coe_Inf
AddSubsemigroup.coe_sInf: โˆ€ {M : Type u_1} [inst : Add M] (S : Set (AddSubsemigroup M)), โ†‘(sInf S) = Set.iInter fun s => Set.iInter fun h => โ†‘s
AddSubsemigroup.coe_sInf
@[
to_additive: โˆ€ {M : Type u_1} [inst : Add M] {S : Set (AddSubsemigroup M)} {x : M}, x โˆˆ sInf S โ†” โˆ€ (p : AddSubsemigroup M), p โˆˆ S โ†’ x โˆˆ p
to_additive
] theorem
mem_sInf: โˆ€ {S : Set (Subsemigroup M)} {x : M}, x โˆˆ sInf S โ†” โˆ€ (p : Subsemigroup M), p โˆˆ S โ†’ x โˆˆ p
mem_sInf
{S :
Set: Type ?u.9014 โ†’ Type ?u.9014
Set
(
Subsemigroup: (M : Type ?u.9015) โ†’ [inst : Mul M] โ†’ Type ?u.9015
Subsemigroup
M: Type ?u.8983
M
)} {
x: M
x
:
M: Type ?u.8983
M
} :
x: M
x
โˆˆ
sInf: {ฮฑ : Type ?u.9032} โ†’ [self : InfSet ฮฑ] โ†’ Set ฮฑ โ†’ ฮฑ
sInf
S โ†” โˆ€
p: ?m.9083
p
โˆˆ S,
x: M
x
โˆˆ
p: ?m.9083
p
:=
Set.mem_iInterโ‚‚: โˆ€ {ฮณ : Type ?u.9139} {ฮน : Sort ?u.9140} {ฮบ : ฮน โ†’ Sort ?u.9141} {x : ฮณ} {s : (i : ฮน) โ†’ ฮบ i โ†’ Set ฮณ}, (x โˆˆ Set.iInter fun i => Set.iInter fun j => s i j) โ†” โˆ€ (i : ฮน) (j : ฮบ i), x โˆˆ s i j
Set.mem_iInterโ‚‚
#align subsemigroup.mem_Inf
Subsemigroup.mem_sInf: โˆ€ {M : Type u_1} [inst : Mul M] {S : Set (Subsemigroup M)} {x : M}, x โˆˆ sInf S โ†” โˆ€ (p : Subsemigroup M), p โˆˆ S โ†’ x โˆˆ p
Subsemigroup.mem_sInf
#align add_subsemigroup.mem_Inf
AddSubsemigroup.mem_sInf: โˆ€ {M : Type u_1} [inst : Add M] {S : Set (AddSubsemigroup M)} {x : M}, x โˆˆ sInf S โ†” โˆ€ (p : AddSubsemigroup M), p โˆˆ S โ†’ x โˆˆ p
AddSubsemigroup.mem_sInf
@[
to_additive: โˆ€ {M : Type u_2} [inst : Add M] {ฮน : Sort u_1} {S : ฮน โ†’ AddSubsemigroup M} {x : M}, (x โˆˆ โจ… i, S i) โ†” โˆ€ (i : ฮน), x โˆˆ S i
to_additive
] theorem
mem_iInf: โˆ€ {M : Type u_2} [inst : Mul M] {ฮน : Sort u_1} {S : ฮน โ†’ Subsemigroup M} {x : M}, (x โˆˆ โจ… i, S i) โ†” โˆ€ (i : ฮน), x โˆˆ S i
mem_iInf
{
ฮน: Sort u_1
ฮน
:
Sort _: Type ?u.9256
Sort
Sort _: Type ?u.9256
_
} {
S: ฮน โ†’ Subsemigroup M
S
:
ฮน: Sort ?u.9256
ฮน
โ†’
Subsemigroup: (M : Type ?u.9261) โ†’ [inst : Mul M] โ†’ Type ?u.9261
Subsemigroup
M: Type ?u.9225
M
} {
x: M
x
:
M: Type ?u.9225
M
} : (
x: M
x
โˆˆ โจ…
i: ?m.9298
i
,
S: ฮน โ†’ Subsemigroup M
S
i: ?m.9298
i
) โ†” โˆ€
i: ?m.9335
i
,
x: M
x
โˆˆ
S: ฮน โ†’ Subsemigroup M
S
i: ?m.9335
i
:=

Goals accomplished! ๐Ÿ™
M: Type u_2

N: Type ?u.9228

A: Type ?u.9231

instโœยน: Mul M

s: Set M

instโœ: Add A

t: Set A

Sโœ: Subsemigroup M

ฮน: Sort u_1

S: ฮน โ†’ Subsemigroup M

x: M


(x โˆˆ โจ… i, S i) โ†” โˆ€ (i : ฮน), x โˆˆ S i

Goals accomplished! ๐Ÿ™
#align subsemigroup.mem_infi
Subsemigroup.mem_iInf: โˆ€ {M : Type u_2} [inst : Mul M] {ฮน : Sort u_1} {S : ฮน โ†’ Subsemigroup M} {x : M}, (x โˆˆ โจ… i, S i) โ†” โˆ€ (i : ฮน), x โˆˆ S i
Subsemigroup.mem_iInf
#align add_subsemigroup.mem_infi
AddSubsemigroup.mem_iInf: โˆ€ {M : Type u_2} [inst : Add M] {ฮน : Sort u_1} {S : ฮน โ†’ AddSubsemigroup M} {x : M}, (x โˆˆ โจ… i, S i) โ†” โˆ€ (i : ฮน), x โˆˆ S i
AddSubsemigroup.mem_iInf
@[
to_additive: โˆ€ {M : Type u_2} [inst : Add M] {ฮน : Sort u_1} {S : ฮน โ†’ AddSubsemigroup M}, โ†‘(โจ… i, S i) = Set.iInter fun i => โ†‘(S i)
to_additive
(attr := simp, norm_cast)] theorem
coe_iInf: โˆ€ {ฮน : Sort u_1} {S : ฮน โ†’ Subsemigroup M}, โ†‘(โจ… i, S i) = Set.iInter fun i => โ†‘(S i)
coe_iInf
{
ฮน: Sort ?u.9690
ฮน
:
Sort _: Type ?u.9690
Sort
Sort _: Type ?u.9690
_
} {
S: ฮน โ†’ Subsemigroup M
S
:
ฮน: Sort ?u.9690
ฮน
โ†’
Subsemigroup: (M : Type ?u.9695) โ†’ [inst : Mul M] โ†’ Type ?u.9695
Subsemigroup
M: Type ?u.9659
M
} : (โ†‘(โจ…
i: ?m.9714
i
,
S: ฮน โ†’ Subsemigroup M
S
i: ?m.9714
i
) :
Set: Type ?u.9707 โ†’ Type ?u.9707
Set
M: Type ?u.9659
M
) = โ‹‚
i: ?m.9829
i
,
S: ฮน โ†’ Subsemigroup M
S
i: ?m.9829
i
:=

Goals accomplished! ๐Ÿ™
M: Type u_2

N: Type ?u.9662

A: Type ?u.9665

instโœยน: Mul M

s: Set M

instโœ: Add A

t: Set A

Sโœ: Subsemigroup M

ฮน: Sort u_1

S: ฮน โ†’ Subsemigroup M


โ†‘(โจ… i, S i) = Set.iInter fun i => โ†‘(S i)

Goals accomplished! ๐Ÿ™
#align subsemigroup.coe_infi
Subsemigroup.coe_iInf: โˆ€ {M : Type u_2} [inst : Mul M] {ฮน : Sort u_1} {S : ฮน โ†’ Subsemigroup M}, โ†‘(โจ… i, S i) = Set.iInter fun i => โ†‘(S i)
Subsemigroup.coe_iInf
#align add_subsemigroup.coe_infi
AddSubsemigroup.coe_iInf: โˆ€ {M : Type u_2} [inst : Add M] {ฮน : Sort u_1} {S : ฮน โ†’ AddSubsemigroup M}, โ†‘(โจ… i, S i) = Set.iInter fun i => โ†‘(S i)
AddSubsemigroup.coe_iInf
/-- subsemigroups of a monoid form a complete lattice. -/ @[
to_additive: {M : Type u_1} โ†’ [inst : Add M] โ†’ CompleteLattice (AddSubsemigroup M)
to_additive
"The `AddSubsemigroup`s of an `AddMonoid` form a complete lattice."]
instance: {M : Type u_1} โ†’ [inst : Mul M] โ†’ CompleteLattice (Subsemigroup M)
instance
:
CompleteLattice: Type ?u.10745 โ†’ Type ?u.10745
CompleteLattice
(
Subsemigroup: (M : Type ?u.10746) โ†’ [inst : Mul M] โ†’ Type ?u.10746
Subsemigroup
M: Type ?u.10714
M
) := {
completeLatticeOfInf: (ฮฑ : Type ?u.10757) โ†’ [H1 : PartialOrder ฮฑ] โ†’ [H2 : InfSet ฮฑ] โ†’ (โˆ€ (s : Set ฮฑ), IsGLB s (sInf s)) โ†’ CompleteLattice ฮฑ
completeLatticeOfInf
(
Subsemigroup: (M : Type ?u.10758) โ†’ [inst : Mul M] โ†’ Type ?u.10758
Subsemigroup
M: Type ?u.10714
M
) fun
_: ?m.10939
_
=>
IsGLB.of_image: โˆ€ {ฮฑ : Type ?u.10942} {ฮฒ : Type ?u.10941} [inst : Preorder ฮฑ] [inst_1 : Preorder ฮฒ] {f : ฮฑ โ†’ ฮฒ}, (โˆ€ {x y : ฮฑ}, f x โ‰ค f y โ†” x โ‰ค y) โ†’ โˆ€ {s : Set ฮฑ} {x : ฮฑ}, IsGLB (f '' s) (f x) โ†’ IsGLB s x
IsGLB.of_image
SetLike.coe_subset_coe: โˆ€ {A : Type ?u.10951} {B : Type ?u.10950} [i : SetLike A B] {S T : A}, โ†‘S โŠ† โ†‘T โ†” S โ‰ค T
SetLike.coe_subset_coe
isGLB_biInf: โˆ€ {ฮฑ : Type ?u.11146} {ฮฒ : Type ?u.11145} [inst : CompleteLattice ฮฑ] {s : Set ฮฒ} {f : ฮฒ โ†’ ฮฑ}, IsGLB (f '' s) (โจ… x, โจ… h, f x)
isGLB_biInf
with le :=
(ยท โ‰ค ยท): Subsemigroup M โ†’ Subsemigroup M โ†’ Prop
(ยท โ‰ค ยท)
lt :=
(ยท < ยท): Subsemigroup M โ†’ Subsemigroup M โ†’ Prop
(ยท < ยท)
bot :=
โŠฅ: ?m.11859
โŠฅ
bot_le := fun
_: ?m.11915
_
_: ?m.11918
_
hx: ?m.11921
hx
=> (
not_mem_bot: โˆ€ {M : Type ?u.11923} [inst : Mul M] {x : M}, ยฌx โˆˆ โŠฅ
not_mem_bot
hx: ?m.11921
hx
).
elim: โˆ€ {C : Sort ?u.11941}, False โ†’ C
elim
top :=
โŠค: ?m.11827
โŠค
le_top := fun
_: ?m.11893
_
x: ?m.11896
x
_: ?m.11899
_
=>
mem_top: โˆ€ {M : Type ?u.11901} [inst : Mul M] (x : M), x โˆˆ โŠค
mem_top
x: ?m.11896
x
inf :=
(ยท โŠ“ ยท): Subsemigroup M โ†’ Subsemigroup M โ†’ Subsemigroup M
(ยท โŠ“ ยท)
sInf :=
InfSet.sInf: {ฮฑ : Type ?u.11750} โ†’ [self : InfSet ฮฑ] โ†’ Set ฮฑ โ†’ ฮฑ
InfSet.sInf
le_inf := fun
_: ?m.11660
_
_: ?m.11663
_
_: ?m.11666
_
ha: ?m.11669
ha
hb: ?m.11672
hb
_: ?m.11675
_
hx: ?m.11678
hx
=> โŸจ
ha: ?m.11669
ha
hx: ?m.11678
hx
,
hb: ?m.11672
hb
hx: ?m.11678
hx
โŸฉ inf_le_left := fun
_: ?m.11618
_
_: ?m.11621
_
_: ?m.11624
_
=>
And.left: โˆ€ {a b : Prop}, a โˆง b โ†’ a
And.left
inf_le_right := fun
_: ?m.11639
_
_: ?m.11642
_
_: ?m.11645
_
=>
And.right: โˆ€ {a b : Prop}, a โˆง b โ†’ b
And.right
} @[
to_additive: โˆ€ {M : Type u_1} [inst : Add M] [inst : Subsingleton (AddSubsemigroup M)], Subsingleton M
to_additive
(attr := simp)] theorem
subsingleton_of_subsingleton: โˆ€ {M : Type u_1} [inst : Mul M] [inst : Subsingleton (Subsemigroup M)], Subsingleton M
subsingleton_of_subsingleton
[
Subsingleton: Sort ?u.12577 โ†’ Prop
Subsingleton
(
Subsemigroup: (M : Type ?u.12578) โ†’ [inst : Mul M] โ†’ Type ?u.12578
Subsemigroup
M: Type ?u.12546
M
)] :
Subsingleton: Sort ?u.12588 โ†’ Prop
Subsingleton
M: Type ?u.12546
M
:=

Goals accomplished! ๐Ÿ™
M: Type u_1

N: Type ?u.12549

A: Type ?u.12552

instโœยฒ: Mul M

s: Set M

instโœยน: Add A

t: Set A

S: Subsemigroup M

instโœ: Subsingleton (Subsemigroup M)


M: Type u_1

N: Type ?u.12549

A: Type ?u.12552

instโœยฒ: Mul M

s: Set M

instโœยน: Add A

t: Set A

S: Subsemigroup M

instโœ: Subsingleton (Subsemigroup M)


allEq
โˆ€ (a b : M), a = b
M: Type u_1

N: Type ?u.12549

A: Type ?u.12552

instโœยฒ: Mul M

s: Set M

instโœยน: Add A

t: Set A

S: Subsemigroup M

instโœ: Subsingleton (Subsemigroup M)


allEq
โˆ€ (a b : M), a = b
M: Type u_1

N: Type ?u.12549

A: Type ?u.12552

instโœยฒ: Mul M

s: Set M

instโœยน: Add A

t: Set A

S: Subsemigroup M

instโœ: Subsingleton (Subsemigroup M)


M: Type u_1

N: Type ?u.12549

A: Type ?u.12552

instโœยฒ: Mul M

s: Set M

instโœยน: Add A

t: Set A

S: Subsemigroup M

instโœ: Subsingleton (Subsemigroup M)

x, y: M


allEq
x = y
M: Type u_1

N: Type ?u.12549

A: Type ?u.12552

instโœยฒ: Mul M

s: Set M

instโœยน: Add A

t: Set A

S: Subsemigroup M

instโœ: Subsingleton (Subsemigroup M)


M: Type u_1

N: Type ?u.12549

A: Type ?u.12552

instโœยฒ: Mul M

s: Set M

instโœยน: Add A

t: Set A

S: Subsemigroup M

instโœ: Subsingleton (Subsemigroup M)

x, y: M


allEq
x = y

Goals accomplished! ๐Ÿ™
M: Type u_1

N: Type ?u.12549

A: Type ?u.12552

instโœยฒ: Mul M

s: Set M

instโœยน: Add A

t: Set A

S: Subsemigroup M

instโœ: Subsingleton (Subsemigroup M)

x, y: M


โˆ€ (a : M), a โˆˆ โŠฅ

Goals accomplished! ๐Ÿ™
M: Type u_1

N: Type ?u.12549

A: Type ?u.12552

instโœยฒ: Mul M

s: Set M

instโœยน: Add A

t: Set A

S: Subsemigroup M

instโœ: Subsingleton (Subsemigroup M)



Goals accomplished! ๐Ÿ™
#align subsemigroup.subsingleton_of_subsingleton
Subsemigroup.subsingleton_of_subsingleton: โˆ€ {M : Type u_1} [inst : Mul M] [inst : Subsingleton (Subsemigroup M)], Subsingleton M
Subsemigroup.subsingleton_of_subsingleton
#align add_subsemigroup.subsingleton_of_subsingleton
AddSubsemigroup.subsingleton_of_subsingleton: โˆ€ {M : Type u_1} [inst : Add M] [inst : Subsingleton (AddSubsemigroup M)], Subsingleton M
AddSubsemigroup.subsingleton_of_subsingleton
@[
to_additive: โˆ€ {M : Type u_1} [inst : Add M] [hn : Nonempty M], Nontrivial (AddSubsemigroup M)
to_additive
]
instance: โˆ€ {M : Type u_1} [inst : Mul M] [hn : Nonempty M], Nontrivial (Subsemigroup M)
instance
[
hn: Nonempty M
hn
:
Nonempty: Sort ?u.13719 โ†’ Prop
Nonempty
M: Type ?u.13688
M
] :
Nontrivial: Type ?u.13722 โ†’ Prop
Nontrivial
(
Subsemigroup: (M : Type ?u.13723) โ†’ [inst : Mul M] โ†’ Type ?u.13723
Subsemigroup
M: Type ?u.13688
M
) := โŸจโŸจ
โŠฅ: ?m.13751
โŠฅ
,
โŠค: ?m.13798
โŠค
, fun
h: ?m.13828
h
=>

Goals accomplished! ๐Ÿ™
M: Type ?u.13688

N: Type ?u.13691

A: Type ?u.13694

instโœยน: Mul M

s: Set M

instโœ: Add A

t: Set A

S: Subsemigroup M

hn: Nonempty M

h: โŠฅ = โŠค


M: Type ?u.13688

N: Type ?u.13691

A: Type ?u.13694

instโœยน: Mul M

s: Set M

instโœ: Add A

t: Set A

S: Subsemigroup M

hn: Nonempty M

h: โŠฅ = โŠค

x: M


intro
M: Type ?u.13688

N: Type ?u.13691

A: Type ?u.13694

instโœยน: Mul M

s: Set M

instโœ: Add A

t: Set A

S: Subsemigroup M

hn: Nonempty M

h: โŠฅ = โŠค


M: Type ?u.13688

N: Type ?u.13691

A: Type ?u.13694

instโœยน: Mul M

s: Set M

instโœ: Add A

t: Set A

S: Subsemigroup M

hn: Nonempty M

h: โŠฅ = โŠค

x: M


intro
M: Type ?u.13688

N: Type ?u.13691

A: Type ?u.13694

instโœยน: Mul M

s: Set M

instโœ: Add A

t: Set A

S: Subsemigroup M

hn: Nonempty M

h: โŠฅ = โŠค



Goals accomplished! ๐Ÿ™
โŸฉโŸฉ /-- The `Subsemigroup` generated by a set. -/ @[
to_additive: {M : Type u_1} โ†’ [inst : Add M] โ†’ Set M โ†’ AddSubsemigroup M
to_additive
"The `AddSubsemigroup` generated by a set"] def
closure: Set M โ†’ Subsemigroup M
closure
(
s: Set M
s
:
Set: Type ?u.14177 โ†’ Type ?u.14177
Set
M: Type ?u.14146
M
) :
Subsemigroup: (M : Type ?u.14180) โ†’ [inst : Mul M] โ†’ Type ?u.14180
Subsemigroup
M: Type ?u.14146
M
:=
sInf: {ฮฑ : Type ?u.14190} โ†’ [self : InfSet ฮฑ] โ†’ Set ฮฑ โ†’ ฮฑ
sInf
{
S: ?m.14212
S
|
s: Set M
s
โŠ†
S: ?m.14212
S
} #align subsemigroup.closure
Subsemigroup.closure: {M : Type u_1} โ†’ [inst : Mul M] โ†’ Set M โ†’ Subsemigroup M
Subsemigroup.closure
#align add_subsemigroup.closure
AddSubsemigroup.closure: {M : Type u_1} โ†’ [inst : Add M] โ†’ Set M โ†’ AddSubsemigroup M
AddSubsemigroup.closure
@[
to_additive: โˆ€ {M : Type u_1} [inst : Add M] {s : Set M} {x : M}, x โˆˆ AddSubsemigroup.closure s โ†” โˆ€ (S : AddSubsemigroup M), s โŠ† โ†‘S โ†’ x โˆˆ S
to_additive
] theorem
mem_closure: โˆ€ {x : M}, x โˆˆ closure s โ†” โˆ€ (S : Subsemigroup M), s โŠ† โ†‘S โ†’ x โˆˆ S
mem_closure
{
x: M
x
:
M: Type ?u.14420
M
} :
x: M
x
โˆˆ
closure: {M : Type ?u.14458} โ†’ [inst : Mul M] โ†’ Set M โ†’ Subsemigroup M
closure
s: Set M
s
โ†” โˆ€ S :
Subsemigroup: (M : Type ?u.14505) โ†’ [inst : Mul M] โ†’ Type ?u.14505
Subsemigroup
M: Type ?u.14420
M
,
s: Set M
s
โŠ† S โ†’
x: M
x
โˆˆ S :=
mem_sInf: โˆ€ {M : Type ?u.14630} [inst : Mul M] {S : Set (Subsemigroup M)} {x : M}, x โˆˆ sInf S โ†” โˆ€ (p : Subsemigroup M), p โˆˆ S โ†’ x โˆˆ p
mem_sInf
#align subsemigroup.mem_closure
Subsemigroup.mem_closure: โˆ€ {M : Type u_1} [inst : Mul M] {s : Set M} {x : M}, x โˆˆ closure s โ†” โˆ€ (S : Subsemigroup M), s โŠ† โ†‘S โ†’ x โˆˆ S
Subsemigroup.mem_closure
#align add_subsemigroup.mem_closure
AddSubsemigroup.mem_closure: โˆ€ {M : Type u_1} [inst : Add M] {s : Set M} {x : M}, x โˆˆ AddSubsemigroup.closure s โ†” โˆ€ (S : AddSubsemigroup M), s โŠ† โ†‘S โ†’ x โˆˆ S
AddSubsemigroup.mem_closure
/-- The subsemigroup generated by a set includes the set. -/ @[
to_additive: โˆ€ {M : Type u_1} [inst : Add M] {s : Set M}, s โŠ† โ†‘(AddSubsemigroup.closure s)
to_additive
(attr := simp) "The `AddSubsemigroup` generated by a set includes the set."] theorem
subset_closure: s โŠ† โ†‘(closure s)
subset_closure
:
s: Set M
s
โŠ†
closure: {M : Type ?u.14746} โ†’ [inst : Mul M] โ†’ Set M โ†’ Subsemigroup M
closure
s: Set M
s
:= fun
_: ?m.14866
_
hx: ?m.14869
hx
=>
mem_closure: โˆ€ {M : Type ?u.14871} [inst : Mul M] {s : Set M} {x : M}, x โˆˆ closure s โ†” โˆ€ (S : Subsemigroup M), s โŠ† โ†‘S โ†’ x โˆˆ S
mem_closure
.
2: โˆ€ {a b : Prop}, (a โ†” b) โ†’ b โ†’ a
2
fun
_: ?m.14923
_
hS: ?m.14926
hS
=>
hS: ?m.14926
hS
hx: ?m.14869
hx
#align subsemigroup.subset_closure
Subsemigroup.subset_closure: โˆ€ {M : Type u_1} [inst : Mul M] {s : Set M}, s โŠ† โ†‘(closure s)
Subsemigroup.subset_closure
#align add_subsemigroup.subset_closure
AddSubsemigroup.subset_closure: โˆ€ {M : Type u_1} [inst : Add M] {s : Set M}, s โŠ† โ†‘(AddSubsemigroup.closure s)
AddSubsemigroup.subset_closure
@[
to_additive: โˆ€ {M : Type u_1} [inst : Add M] {s : Set M} {P : M}, ยฌP โˆˆ AddSubsemigroup.closure s โ†’ ยฌP โˆˆ s
to_additive
] theorem
not_mem_of_not_mem_closure: โˆ€ {P : M}, ยฌP โˆˆ closure s โ†’ ยฌP โˆˆ s
not_mem_of_not_mem_closure
{
P: M
P
:
M: Type ?u.15030
M
} (hP :
P: M
P
โˆ‰
closure: {M : Type ?u.15068} โ†’ [inst : Mul M] โ†’ Set M โ†’ Subsemigroup M
closure
s: Set M
s
) :
P: M
P
โˆ‰
s: Set M
s
:= fun
h: ?m.15135
h
=> hP (
subset_closure: โˆ€ {M : Type ?u.15137} [inst : Mul M] {s : Set M}, s โŠ† โ†‘(closure s)
subset_closure
h: ?m.15135
h
) #align subsemigroup.not_mem_of_not_mem_closure
Subsemigroup.not_mem_of_not_mem_closure: โˆ€ {M : Type u_1} [inst : Mul M] {s : Set M} {P : M}, ยฌP โˆˆ closure s โ†’ ยฌP โˆˆ s
Subsemigroup.not_mem_of_not_mem_closure
#align add_subsemigroup.not_mem_of_not_mem_closure
AddSubsemigroup.not_mem_of_not_mem_closure: โˆ€ {M : Type u_1} [inst : Add M] {s : Set M} {P : M}, ยฌP โˆˆ AddSubsemigroup.closure s โ†’ ยฌP โˆˆ s
AddSubsemigroup.not_mem_of_not_mem_closure
variable {
S: ?m.15253
S
} open Set /-- A subsemigroup `S` includes `closure s` if and only if it includes `s`. -/ @[
to_additive: โˆ€ {M : Type u_1} [inst : Add M] {s : Set M} {S : AddSubsemigroup M}, AddSubsemigroup.closure s โ‰ค S โ†” s โŠ† โ†‘S
to_additive
(attr := simp) "An additive subsemigroup `S` includes `closure s` if and only if it includes `s`"] theorem
closure_le: closure s โ‰ค S โ†” s โŠ† โ†‘S
closure_le
:
closure: {M : Type ?u.15288} โ†’ [inst : Mul M] โ†’ Set M โ†’ Subsemigroup M
closure
s: Set M
s
โ‰ค S โ†”
s: Set M
s
โŠ† S := โŸจ
Subset.trans: โˆ€ {ฮฑ : Type ?u.15448} {a b c : Set ฮฑ}, a โŠ† b โ†’ b โŠ† c โ†’ a โŠ† c
Subset.trans
subset_closure: โˆ€ {M : Type ?u.15480} [inst : Mul M] {s : Set M}, s โŠ† โ†‘(closure s)
subset_closure
, fun
h: ?m.15525
h
=>
sInf_le: โˆ€ {ฮฑ : Type ?u.15527} [inst : CompleteSemilatticeInf ฮฑ] {s : Set ฮฑ} {a : ฮฑ}, a โˆˆ s โ†’ sInf s โ‰ค a
sInf_le
h: ?m.15525
h
โŸฉ #align subsemigroup.closure_le
Subsemigroup.closure_le: โˆ€ {M : Type u_1} [inst : Mul M] {s : Set M} {S : Subsemigroup M}, closure s โ‰ค S โ†” s โŠ† โ†‘S
Subsemigroup.closure_le
#align add_subsemigroup.closure_le
AddSubsemigroup.closure_le: โˆ€ {M : Type u_1} [inst : Add M] {s : Set M} {S : AddSubsemigroup M}, AddSubsemigroup.closure s โ‰ค S โ†” s โŠ† โ†‘S
AddSubsemigroup.closure_le
/-- subsemigroup closure of a set is monotone in its argument: if `s โŠ† t`, then `closure s โ‰ค closure t`. -/ @[
to_additive: โˆ€ {M : Type u_1} [inst : Add M] โฆƒs t : Set Mโฆ„, s โŠ† t โ†’ AddSubsemigroup.closure s โ‰ค AddSubsemigroup.closure t
to_additive
"Additive subsemigroup closure of a set is monotone in its argument: if `s โŠ† t`, then `closure s โ‰ค closure t`"] theorem
closure_mono: โˆ€ {M : Type u_1} [inst : Mul M] โฆƒs t : Set Mโฆ„, s โŠ† t โ†’ closure s โ‰ค closure t
closure_mono
โฆƒ
s: Set M
s
t: Set M
t
:
Set: Type ?u.15702 โ†’ Type ?u.15702
Set
M: Type ?u.15668
M
โฆ„ (
h: s โŠ† t
h
:
s: Set M
s
โŠ†
t: Set M
t
) :
closure: {M : Type ?u.15725} โ†’ [inst : Mul M] โ†’ Set M โ†’ Subsemigroup M
closure
s: Set M
s
โ‰ค
closure: {M : Type ?u.15736} โ†’ [inst : Mul M] โ†’ Set M โ†’ Subsemigroup M
closure
t: Set M
t
:=
closure_le: โˆ€ {M : Type ?u.15790} [inst : Mul M] {s : Set M} {S : Subsemigroup M}, closure s โ‰ค S โ†” s โŠ† โ†‘S
closure_le
.
2: โˆ€ {a b : Prop}, (a โ†” b) โ†’ b โ†’ a
2
<|
Subset.trans: โˆ€ {ฮฑ : Type ?u.15830} {a b c : Set ฮฑ}, a โŠ† b โ†’ b โŠ† c โ†’ a โŠ† c
Subset.trans
h: s โŠ† t
h
subset_closure: โˆ€ {M : Type ?u.15843} [inst : Mul M] {s : Set M}, s โŠ† โ†‘(closure s)
subset_closure
#align subsemigroup.closure_mono
Subsemigroup.closure_mono: โˆ€ {M : Type u_1} [inst : Mul M] โฆƒs t : Set Mโฆ„, s โŠ† t โ†’ closure s โ‰ค closure t
Subsemigroup.closure_mono
#align add_subsemigroup.closure_mono
AddSubsemigroup.closure_mono: โˆ€ {M : Type u_1} [inst : Add M] โฆƒs t : Set Mโฆ„, s โŠ† t โ†’ AddSubsemigroup.closure s โ‰ค AddSubsemigroup.closure t
AddSubsemigroup.closure_mono
@[
to_additive: โˆ€ {M : Type u_1} [inst : Add M] {s : Set M} {S : AddSubsemigroup M}, s โŠ† โ†‘S โ†’ S โ‰ค AddSubsemigroup.closure s โ†’ AddSubsemigroup.closure s = S
to_additive
] theorem
closure_eq_of_le: โˆ€ {M : Type u_1} [inst : Mul M] {s : Set M} {S : Subsemigroup M}, s โŠ† โ†‘S โ†’ S โ‰ค closure s โ†’ closure s = S
closure_eq_of_le
(
hโ‚: s โŠ† โ†‘S
hโ‚
:
s: Set M
s
โŠ† S) (
hโ‚‚: S โ‰ค closure s
hโ‚‚
: S โ‰ค
closure: {M : Type ?u.16050} โ†’ [inst : Mul M] โ†’ Set M โ†’ Subsemigroup M
closure
s: Set M
s
) :
closure: {M : Type ?u.16100} โ†’ [inst : Mul M] โ†’ Set M โ†’ Subsemigroup M
closure
s: Set M
s
= S :=
le_antisymm: โˆ€ {ฮฑ : Type ?u.16109} [inst : PartialOrder ฮฑ] {a b : ฮฑ}, a โ‰ค b โ†’ b โ‰ค a โ†’ a = b
le_antisymm
(
closure_le: โˆ€ {M : Type ?u.16140} [inst : Mul M] {s : Set M} {S : Subsemigroup M}, closure s โ‰ค S โ†” s โŠ† โ†‘S
closure_le
.
2: โˆ€ {a b : Prop}, (a โ†” b) โ†’ b โ†’ a
2
hโ‚: s โŠ† โ†‘S
hโ‚
)
hโ‚‚: S โ‰ค closure s
hโ‚‚
#align subsemigroup.closure_eq_of_le
Subsemigroup.closure_eq_of_le: โˆ€ {M : Type u_1} [inst : Mul M] {s : Set M} {S : Subsemigroup M}, s โŠ† โ†‘S โ†’ S โ‰ค closure s โ†’ closure s = S
Subsemigroup.closure_eq_of_le
#align add_subsemigroup.closure_eq_of_le
AddSubsemigroup.closure_eq_of_le: โˆ€ {M : Type u_1} [inst : Add M] {s : Set M} {S : AddSubsemigroup M}, s โŠ† โ†‘S โ†’ S โ‰ค AddSubsemigroup.closure s โ†’ AddSubsemigroup.closure s = S
AddSubsemigroup.closure_eq_of_le
variable (
S: ?m.16279
S
) /-- An induction principle for closure membership. If `p` holds for all elements of `s`, and is preserved under multiplication, then `p` holds for all elements of the closure of `s`. -/ @[
to_additive: โˆ€ {M : Type u_1} [inst : Add M] {s : Set M} {p : M โ†’ Prop} {x : M}, x โˆˆ AddSubsemigroup.closure s โ†’ (โˆ€ (x : M), x โˆˆ s โ†’ p x) โ†’ (โˆ€ (x y : M), p x โ†’ p y โ†’ p (x + y)) โ†’ p x
to_additive
(attr := elab_as_elim) "An induction principle for additive closure membership. If `p` holds for all elements of `s`, and is preserved under addition, then `p` holds for all elements of the additive closure of `s`."] theorem
closure_induction: โˆ€ {p : M โ†’ Prop} {x : M}, x โˆˆ closure s โ†’ (โˆ€ (x : M), x โˆˆ s โ†’ p x) โ†’ (โˆ€ (x y : M), p x โ†’ p y โ†’ p (x * y)) โ†’ p x
closure_induction
{
p: M โ†’ Prop
p
:
M: Type ?u.16282
M
โ†’
Prop: Type
Prop
} {
x: M
x
} (h :
x: ?m.16317
x
โˆˆ
closure: {M : Type ?u.16337} โ†’ [inst : Mul M] โ†’ Set M โ†’ Subsemigroup M
closure
s: Set M
s
) (
Hs: โˆ€ (x : M), x โˆˆ s โ†’ p x
Hs
: โˆ€
x: ?m.16390
x
โˆˆ
s: Set M
s
,
p: M โ†’ Prop
p
x: ?m.16390
x
) (
Hmul: โˆ€ (x y : M), p x โ†’ p y โ†’ p (x * y)
Hmul
: โˆ€
x: ?m.16427
x
y: ?m.16430
y
,
p: M โ†’ Prop
p
x: ?m.16427
x
โ†’
p: M โ†’ Prop
p
y: ?m.16430
y
โ†’
p: M โ†’ Prop
p
(
x: ?m.16427
x
*
y: ?m.16430
y
)) :
p: M โ†’ Prop
p
x: ?m.16317
x
:= (@
closure_le: โˆ€ {M : Type ?u.16483} [inst : Mul M] {s : Set M} {S : Subsemigroup M}, closure s โ‰ค S โ†” s โŠ† โ†‘S
closure_le
_: Type ?u.16483
_
_
_: Set ?m.16484
_
โŸจ
p: M โ†’ Prop
p
,
Hmul: โˆ€ (x y : M), p x โ†’ p y โ†’ p (x * y)
Hmul
_: M
_
_: M
_
โŸฉ).
2: โˆ€ {a b : Prop}, (a โ†” b) โ†’ b โ†’ a
2
Hs: โˆ€ (x : M), x โˆˆ s โ†’ p x
Hs
h #align subsemigroup.closure_induction
Subsemigroup.closure_induction: โˆ€ {M : Type u_1} [inst : Mul M] {s : Set M} {p : M โ†’ Prop} {x : M}, x โˆˆ closure s โ†’ (โˆ€ (x : M), x โˆˆ s โ†’ p x) โ†’ (โˆ€ (x y : M), p x โ†’ p y โ†’ p (x * y)) โ†’ p x
Subsemigroup.closure_induction
#align add_subsemigroup.closure_induction
AddSubsemigroup.closure_induction: โˆ€ {M : Type u_1} [inst : Add M] {s : Set M} {p : M โ†’ Prop} {x : M}, x โˆˆ AddSubsemigroup.closure s โ†’ (โˆ€ (x : M), x โˆˆ s โ†’ p x) โ†’ (โˆ€ (x y : M), p x โ†’ p y โ†’ p (x + y)) โ†’ p x
AddSubsemigroup.closure_induction
/-- A dependent version of `Subsemigroup.closure_induction`. -/ @[
to_additive: โˆ€ {M : Type u_1} [inst : Add M] (s : Set M) {p : (x : M) โ†’ x โˆˆ AddSubsemigroup.closure s โ†’ Prop}, (โˆ€ (x : M) (h : x โˆˆ s), p x (_ : x โˆˆ โ†‘(AddSubsemigroup.closure s))) โ†’ (โˆ€ (x : M) (hx : x โˆˆ AddSubsemigroup.closure s) (y : M) (hy : y โˆˆ AddSubsemigroup.closure s), p x hx โ†’ p y hy โ†’ p (x + y) (_ : x + y โˆˆ AddSubsemigroup.closure s)) โ†’ โˆ€ {x : M} (hx : x โˆˆ AddSubsemigroup.closure s), p x hx
to_additive
(attr := elab_as_elim) "A dependent version of `AddSubsemigroup.closure_induction`. "] theorem
closure_induction': โˆ€ (s : Set M) {p : (x : M) โ†’ x โˆˆ closure s โ†’ Prop}, (โˆ€ (x : M) (h : x โˆˆ s), p x (_ : x โˆˆ โ†‘(closure s))) โ†’ (โˆ€ (x : M) (hx : x โˆˆ closure s) (y : M) (hy : y โˆˆ closure s), p x hx โ†’ p y hy โ†’ p (x * y) (_ : x * y โˆˆ closure s)) โ†’ โˆ€ {x : M} (hx : x โˆˆ closure s), p x hx
closure_induction'
(
s: Set M
s
:
Set: Type ?u.16723 โ†’ Type ?u.16723
Set
M: Type ?u.16692
M
) {
p: (x : M) โ†’ x โˆˆ closure s โ†’ Prop
p
: โˆ€
x: ?m.16727
x
,
x: ?m.16727
x
โˆˆ
closure: {M : Type ?u.16748} โ†’ [inst : Mul M] โ†’ Set M โ†’ Subsemigroup M
closure
s: Set M
s
โ†’
Prop: Type
Prop
} (
Hs: โˆ€ (x : M) (h : x โˆˆ s), p x (_ : x โˆˆ โ†‘(closure s))
Hs
: โˆ€ (
x: ?m.16802
x
) (
h: x โˆˆ s
h
:
x: ?m.16802
x
โˆˆ
s: Set M
s
),
p: (x : M) โ†’ x โˆˆ closure s โ†’ Prop
p
x: ?m.16802
x
(
subset_closure: โˆ€ {M : Type ?u.16836} [inst : Mul M] {s : Set M}, s โŠ† โ†‘(closure s)
subset_closure
h: x โˆˆ s
h
)) (
Hmul: โˆ€ (x : M) (hx : x โˆˆ closure s) (y : M) (hy : y โˆˆ closure s), p x hx โ†’ p y hy โ†’ p (x * y) (_ : x * y โˆˆ closure s)
Hmul
: โˆ€
x: ?m.16882
x
hx: ?m.16885
hx
y: ?m.16888
y
hy: ?m.16891
hy
,
p: (x : M) โ†’ x โˆˆ closure s โ†’ Prop
p
x: ?m.16882
x
hx: ?m.16885
hx
โ†’
p: (x : M) โ†’ x โˆˆ closure s โ†’ Prop
p
y: ?m.16888
y
hy: ?m.16891
hy
โ†’
p: (x : M) โ†’ x โˆˆ closure s โ†’ Prop
p
(
x: ?m.16882
x
*
y: ?m.16888
y
) (
mul_mem: โˆ€ {S : Type ?u.16937} {M : Type ?u.16936} [inst : Mul M] [inst_1 : SetLike S M] [self : MulMemClass S M] {s : S} {a b : M}, a โˆˆ s โ†’ b โˆˆ s โ†’ a * b โˆˆ s
mul_mem
hx: ?m.16885
hx
hy: ?m.16891
hy
)) {
x: ?m.17011
x
} (hx :
x: ?m.17011
x
โˆˆ
closure: {M : Type ?u.17031} โ†’ [inst : Mul M] โ†’ Set M โ†’ Subsemigroup M
closure
s: Set M
s
) :
p: (x : M) โ†’ x โˆˆ closure s โ†’ Prop
p
x: ?m.17011
x
hx :=

Goals accomplished! ๐Ÿ™
M: Type u_1

N: Type ?u.16695

A: Type ?u.16698

instโœยน: Mul M

sโœ: Set M

instโœ: Add A

t: Set A

S: Subsemigroup M

s: Set M

p: (x : M) โ†’ x โˆˆ closure s โ†’ Prop

Hs: โˆ€ (x : M) (h : x โˆˆ s), p x (_ : x โˆˆ โ†‘(closure s))

Hmul: โˆ€ (x : M) (hx : x โˆˆ closure s) (y : M) (hy : y โˆˆ closure s), p x hx โ†’ p y hy โ†’ p (x * y) (_ : x * y โˆˆ closure s)

x: M

hx: x โˆˆ closure s


p x hx
M: Type u_1

N: Type ?u.16695

A: Type ?u.16698

instโœยน: Mul M

sโœ: Set M

instโœ: Add A

t: Set A

S: Subsemigroup M

s: Set M

p: (x : M) โ†’ x โˆˆ closure s โ†’ Prop

Hs: โˆ€ (x : M) (h : x โˆˆ s), p x (_ : x โˆˆ โ†‘(closure s))

Hmul: โˆ€ (x : M) (hx : x โˆˆ closure s) (y : M) (hy : y โˆˆ closure s), p x hx โ†’ p y hy โ†’ p (x * y) (_ : x * y โˆˆ closure s)

x: M

hx: x โˆˆ closure s


โˆƒ x_1, p x x_1
M: Type u_1

N: Type ?u.16695

A: Type ?u.16698

instโœยน: Mul M

sโœ: Set M

instโœ: Add A

t: Set A

S: Subsemigroup M

s: Set M

p: (x : M) โ†’ x โˆˆ closure s โ†’ Prop

Hs: โˆ€ (x : M) (h : x โˆˆ s), p x (_ : x โˆˆ โ†‘(closure s))

Hmul: โˆ€ (x : M) (hx : x โˆˆ closure s) (y : M) (hy : y โˆˆ closure s), p x hx โ†’ p y hy โ†’ p (x * y) (_ : x * y โˆˆ closure s)

x: M

hx: x โˆˆ closure s


p x hx

Goals accomplished! ๐Ÿ™
#align subsemigroup.closure_induction'
Subsemigroup.closure_induction': โˆ€ {M : Type u_1} [inst : Mul M] (s : Set M) {p : (x : M) โ†’ x โˆˆ closure s โ†’ Prop}, (โˆ€ (x : M) (h : x โˆˆ s), p x (_ : x โˆˆ โ†‘(closure s))) โ†’ (โˆ€ (x : M) (hx : x โˆˆ closure s) (y : M) (hy : y โˆˆ closure s), p x hx โ†’ p y hy โ†’ p (x * y) (_ : x * y โˆˆ closure s)) โ†’ โˆ€ {x : M} (hx : x โˆˆ closure s), p x hx
Subsemigroup.closure_induction'
#align add_subsemigroup.closure_induction'
AddSubsemigroup.closure_induction': โˆ€ {M : Type u_1} [inst : Add M] (s : Set M) {p : (x : M) โ†’ x โˆˆ AddSubsemigroup.closure s โ†’ Prop}, (โˆ€ (x : M) (h : x โˆˆ s), p x (_ : x โˆˆ โ†‘(AddSubsemigroup.closure s))) โ†’ (โˆ€ (x : M) (hx : x โˆˆ AddSubsemigroup.closure s) (y : M) (hy : y โˆˆ AddSubsemigroup.closure s), p x hx โ†’ p y hy โ†’ p (x + y) (_ : x + y โˆˆ AddSubsemigroup.closure s)) โ†’ โˆ€ {x : M} (hx : x โˆˆ AddSubsemigroup.closure s), p x hx
AddSubsemigroup.closure_induction'
/-- An induction principle for closure membership for predicates with two arguments. -/ @[
to_additive: โˆ€ {M : Type u_1} [inst : Add M] {s : Set M} {p : M โ†’ M โ†’ Prop} {x y : M}, x โˆˆ AddSubsemigroup.closure s โ†’ y โˆˆ AddSubsemigroup.closure s โ†’ (โˆ€ (x : M), x โˆˆ s โ†’ โˆ€ (y : M), y โˆˆ s โ†’ p x y) โ†’ (โˆ€ (x y z : M), p x z โ†’ p y z โ†’ p (x + y) z) โ†’ (โˆ€ (x y z : M), p z x โ†’ p z y โ†’ p z (x + y)) โ†’ p x y
to_additive
(attr := elab_as_elim) "An induction principle for additive closure membership for predicates with two arguments."] theorem
closure_inductionโ‚‚: โˆ€ {p : M โ†’ M โ†’ Prop} {x y : M}, x โˆˆ closure s โ†’ y โˆˆ closure s โ†’ (โˆ€ (x : M), x โˆˆ s โ†’ โˆ€ (y : M), y โˆˆ s โ†’ p x y) โ†’ (โˆ€ (x y z : M), p x z โ†’ p y z โ†’ p (x * y) z) โ†’ (โˆ€ (x y z : M), p z x โ†’ p z y โ†’ p z (x * y)) โ†’ p x y
closure_inductionโ‚‚
{
p: M โ†’ M โ†’ Prop
p
:
M: Type ?u.17690
M
โ†’
M: Type ?u.17690
M
โ†’
Prop: Type
Prop
} {
x: ?m.17727
x
} {
y: M
y
:
M: Type ?u.17690
M
} (hx :
x: ?m.17727
x
โˆˆ
closure: {M : Type ?u.17749} โ†’ [inst : Mul M] โ†’ Set M โ†’ Subsemigroup M
closure
s: Set M
s
) (hy :
y: M
y
โˆˆ
closure: {M : Type ?u.17818} โ†’ [inst : Mul M] โ†’ Set M โ†’ Subsemigroup M
closure
s: Set M
s
) (
Hs: โˆ€ (x : M), x โˆˆ s โ†’ โˆ€ (y : M), y โˆˆ s โ†’ p x y
Hs
: โˆ€
x: ?m.17851
x
โˆˆ
s: Set M
s
, โˆ€
y: ?m.17886
y
โˆˆ
s: Set M
s
,
p: M โ†’ M โ†’ Prop
p
x: ?m.17851
x
y: ?m.17886
y
) (
Hmul_left: โˆ€ (x y z : M), p x z โ†’ p y z โ†’ p (x * y) z
Hmul_left
: โˆ€
x: ?m.17922
x
y: ?m.17925
y
z: ?m.17928
z
,
p: M โ†’ M โ†’ Prop
p
x: ?m.17922
x
z: ?m.17928
z
โ†’
p: M โ†’ M โ†’ Prop
p
y: ?m.17925
y
z: ?m.17928
z
โ†’
p: M โ†’ M โ†’ Prop
p
(
x: ?m.17922
x
*
y: ?m.17925
y
)
z: ?m.17928
z
) (
Hmul_right: โˆ€ (x y z : M), p z x โ†’ p z y โ†’ p z (x * y)
Hmul_right
: โˆ€
x: ?m.17976
x
y: ?m.17979
y
z: ?m.17982
z
,
p: M โ†’ M โ†’ Prop
p
z: ?m.17982
z
x: ?m.17976
x
โ†’
p: M โ†’ M โ†’ Prop
p
z: ?m.17982
z
y: ?m.17979
y
โ†’
p: M โ†’ M โ†’ Prop
p
z: ?m.17982
z
(
x: ?m.17976
x
*
y: ?m.17979
y
)) :
p: M โ†’ M โ†’ Prop
p
x: ?m.17727
x
y: M
y
:=
closure_induction: โˆ€ {M : Type ?u.18024} [inst : Mul M] {s : Set M} {p : M โ†’ Prop} {x : M}, x โˆˆ closure s โ†’ (โˆ€ (x : M), x โˆˆ s โ†’ p x) โ†’ (โˆ€ (x y : M), p x โ†’ p y โ†’ p (x * y)) โ†’ p x
closure_induction
hx (fun
x: ?m.18093
x
xs: ?m.18096
xs
=>
closure_induction: โˆ€ {M : Type ?u.18098} [inst : Mul M] {s : Set M} {p : M โ†’ Prop} {x : M}, x โˆˆ closure s โ†’ (โˆ€ (x : M), x โˆˆ s โ†’ p x) โ†’ (โˆ€ (x y : M), p x โ†’ p y โ†’ p (x * y)) โ†’ p x
closure_induction
hy (
Hs: โˆ€ (x : M), x โˆˆ s โ†’ โˆ€ (y : M), y โˆˆ s โ†’ p x y
Hs
x: ?m.18093
x
xs: ?m.18096
xs
) fun
z: ?m.18184
z
_: ?m.18187
_
hโ‚: ?m.18190
hโ‚
hโ‚‚: ?m.18193
hโ‚‚
=>
Hmul_right: โˆ€ (x y z : M), p z x โ†’ p z y โ†’ p z (x * y)
Hmul_right
z: ?m.18184
z
_: M
_
_: M
_
hโ‚: ?m.18190
hโ‚
hโ‚‚: ?m.18193
hโ‚‚
) fun
_: ?m.18153
_
_: ?m.18156
_
hโ‚: ?m.18159
hโ‚
hโ‚‚: ?m.18162
hโ‚‚
=>
Hmul_left: โˆ€ (x y z : M), p x z โ†’ p y z โ†’ p (x * y) z
Hmul_left
_: M
_
_: M
_
_: M
_
hโ‚: ?m.18159
hโ‚
hโ‚‚: ?m.18162
hโ‚‚
#align subsemigroup.closure_inductionโ‚‚
Subsemigroup.closure_inductionโ‚‚: โˆ€ {M : Type u_1} [inst : Mul M] {s : Set M} {p : M โ†’ M โ†’ Prop} {x y : M}, x โˆˆ closure s โ†’ y โˆˆ closure s โ†’ (โˆ€ (x : M), x โˆˆ s โ†’ โˆ€ (y : M), y โˆˆ s โ†’ p x y) โ†’ (โˆ€ (x y z : M), p x z โ†’ p y z โ†’ p (x * y) z) โ†’ (โˆ€ (x y z : M), p z x โ†’ p z y โ†’ p z (x * y)) โ†’ p x y
Subsemigroup.closure_inductionโ‚‚
#align add_subsemigroup.closure_inductionโ‚‚
AddSubsemigroup.closure_inductionโ‚‚: โˆ€ {M : Type u_1} [inst : Add M] {s : Set M} {p : M โ†’ M โ†’ Prop} {x y : M}, x โˆˆ AddSubsemigroup.closure s โ†’ y โˆˆ AddSubsemigroup.closure s โ†’ (โˆ€ (x : M), x โˆˆ s โ†’ โˆ€ (y : M), y โˆˆ s โ†’ p x y) โ†’ (โˆ€ (x y z : M), p x z โ†’ p y z โ†’ p (x + y) z) โ†’ (โˆ€ (x y z : M), p z x โ†’ p z y โ†’ p z (x + y)) โ†’ p x y
AddSubsemigroup.closure_inductionโ‚‚
/-- If `s` is a dense set in a magma `M`, `Subsemigroup.closure s = โŠค`, then in order to prove that some predicate `p` holds for all `x : M` it suffices to verify `p x` for `x โˆˆ s`, and verify that `p x` and `p y` imply `p (x * y)`. -/ @[
to_additive: โˆ€ {M : Type u_1} [inst : Add M] {p : M โ†’ Prop} (x : M) {s : Set M}, AddSubsemigroup.closure s = โŠค โ†’ (โˆ€ (x : M), x โˆˆ s โ†’ p x) โ†’ (โˆ€ (x y : M), p x โ†’ p y โ†’ p (x + y)) โ†’ p x
to_additive
(attr := elab_as_elim) "If `s` is a dense set in an additive monoid `M`, `AddSubsemigroup.closure s = โŠค`, then in order to prove that some predicate `p` holds for all `x : M` it suffices to verify `p x` for `x โˆˆ s`, and verify that `p x` and `p y` imply `p (x + y)`."] theorem
dense_induction: โˆ€ {p : M โ†’ Prop} (x : M) {s : Set M}, closure s = โŠค โ†’ (โˆ€ (x : M), x โˆˆ s โ†’ p x) โ†’ (โˆ€ (x y : M), p x โ†’ p y โ†’ p (x * y)) โ†’ p x
dense_induction
{
p: M โ†’ Prop
p
:
M: Type ?u.18434
M
โ†’
Prop: Type
Prop
} (
x: M
x
:
M: Type ?u.18434
M
) {
s: Set M
s
:
Set: Type ?u.18471 โ†’ Type ?u.18471
Set
M: Type ?u.18434
M
} (hs :
closure: {M : Type ?u.18475} โ†’ [inst : Mul M] โ†’ Set M โ†’ Subsemigroup M
closure
s: Set M
s
=
โŠค: ?m.18488
โŠค
) (
Hs: โˆ€ (x : M), x โˆˆ s โ†’ p x
Hs
: โˆ€
x: ?m.18539
x
โˆˆ
s: Set M
s
,
p: M โ†’ Prop
p
x: ?m.18539
x
) (
Hmul: โˆ€ (x y : M), p x โ†’ p y โ†’ p (x * y)
Hmul
: โˆ€
x: ?m.18578
x
y: ?m.18581
y
,
p: M โ†’ Prop
p
x: ?m.18578
x
โ†’
p: M โ†’ Prop
p
y: ?m.18581
y
โ†’
p: M โ†’ Prop
p
(
x: ?m.18578
x
*
y: ?m.18581
y
)) :
p: M โ†’ Prop
p
x: M
x
:=

Goals accomplished! ๐Ÿ™
M: Type u_1

N: Type ?u.18437

A: Type ?u.18440

instโœยน: Mul M

sโœ: Set M

instโœ: Add A

t: Set A

S: Subsemigroup M

p: M โ†’ Prop

x: M

s: Set M

hs: closure s = โŠค

Hs: โˆ€ (x : M), x โˆˆ s โ†’ p x

Hmul: โˆ€ (x y : M), p x โ†’ p y โ†’ p (x * y)


p x
M: Type u_1

N: Type ?u.18437

A: Type ?u.18440

instโœยน: Mul M

sโœ: Set M

instโœ: Add A

t: Set A

S: Subsemigroup M

p: M โ†’ Prop

x: M

s: Set M

hs: closure s = โŠค

Hs: โˆ€ (x : M), x โˆˆ s โ†’ p x

Hmul: โˆ€ (x y : M), p x โ†’ p y โ†’ p (x * y)

this: โˆ€ (x : M), x โˆˆ closure s โ†’ p x


p x
M: Type u_1

N: Type ?u.18437

A: Type ?u.18440

instโœยน: Mul M

sโœ: Set M

instโœ: Add A

t: Set A

S: Subsemigroup M

p: M โ†’ Prop

x: M

s: Set M

hs: closure s = โŠค

Hs: โˆ€ (x : M), x โˆˆ s โ†’ p x

Hmul: โˆ€ (x y : M), p x โ†’ p y โ†’ p (x * y)


p x

Goals accomplished! ๐Ÿ™
#align subsemigroup.dense_induction
Subsemigroup.dense_induction: โˆ€ {M : Type u_1} [inst : Mul M] {p : M โ†’ Prop} (x : M) {s : Set M}, closure s = โŠค โ†’ (โˆ€ (x : M), x โˆˆ s โ†’ p x) โ†’ (โˆ€ (x y : M), p x โ†’ p y โ†’ p (x * y)) โ†’ p x
Subsemigroup.dense_induction
#align add_subsemigroup.dense_induction
AddSubsemigroup.dense_induction: โˆ€ {M : Type u_1} [inst : Add M] {p : M โ†’ Prop} (x : M) {s : Set M}, AddSubsemigroup.closure s = โŠค โ†’ (โˆ€ (x : M), x โˆˆ s โ†’ p x) โ†’ (โˆ€ (x y : M), p x โ†’ p y โ†’ p (x + y)) โ†’ p x
AddSubsemigroup.dense_induction
variable (
M: ?m.19120
M
) /-- `closure` forms a Galois insertion with the coercion to set. -/ @[
to_additive: (M : Type u_1) โ†’ [inst : Add M] โ†’ GaloisInsertion AddSubsemigroup.closure SetLike.coe
to_additive
"`closure` forms a Galois insertion with the coercion to set."] protected def
gi: GaloisInsertion closure SetLike.coe
gi
:
GaloisInsertion: {ฮฑ : Type ?u.19155} โ†’ {ฮฒ : Type ?u.19154} โ†’ [inst : Preorder ฮฑ] โ†’ [inst : Preorder ฮฒ] โ†’ (ฮฑ โ†’ ฮฒ) โ†’ (ฮฒ โ†’ ฮฑ) โ†’ Type (max?u.19155?u.19154)
GaloisInsertion
(@
closure: {M : Type ?u.19190} โ†’ [inst : Mul M] โ†’ Set M โ†’ Subsemigroup M
closure
M: Type ?u.19123
M
_)
SetLike.coe: {A : Type ?u.19204} โ†’ {B : outParam (Type ?u.19203)} โ†’ [self : SetLike A B] โ†’ A โ†’ Set B
SetLike.coe
:=
GaloisConnection.toGaloisInsertion: {ฮฑ : Type ?u.19300} โ†’ {ฮฒ : Type ?u.19299} โ†’ [inst : Preorder ฮฑ] โ†’ [inst_1 : Preorder ฮฒ] โ†’ {l : ฮฑ โ†’ ฮฒ} โ†’ {u : ฮฒ โ†’ ฮฑ} โ†’ GaloisConnection l u โ†’ (โˆ€ (b : ฮฒ), b โ‰ค l (u b)) โ†’ GaloisInsertion l u
GaloisConnection.toGaloisInsertion
(fun
_: ?m.19348
_
_: ?m.19351
_
=>
closure_le: โˆ€ {M : Type ?u.19353} [inst : Mul M] {s : Set M} {S : Subsemigroup M}, closure s โ‰ค S โ†” s โŠ† โ†‘S
closure_le
) fun
_: ?m.19390
_
=>
subset_closure: โˆ€ {M : Type ?u.19392} [inst : Mul M] {s : Set M}, s โŠ† โ†‘(closure s)
subset_closure
#align subsemigroup.gi
Subsemigroup.gi: (M : Type u_1) โ†’ [inst : Mul M] โ†’ GaloisInsertion closure SetLike.coe
Subsemigroup.gi
#align add_subsemigroup.gi
AddSubsemigroup.gi: (M : Type u_1) โ†’ [inst : Add M] โ†’ GaloisInsertion AddSubsemigroup.closure SetLike.coe
AddSubsemigroup.gi
variable {
M: ?m.19603
M
} /-- Closure of a subsemigroup `S` equals `S`. -/ @[
to_additive: โˆ€ {M : Type u_1} [inst : Add M] (S : AddSubsemigroup M), AddSubsemigroup.closure โ†‘S = S
to_additive
(attr := simp) "Additive closure of an additive subsemigroup `S` equals `S`"] theorem
closure_eq: โˆ€ {M : Type u_1} [inst : Mul M] (S : Subsemigroup M), closure โ†‘S = S
closure_eq
:
closure: {M : Type ?u.19638} โ†’ [inst : Mul M] โ†’ Set M โ†’ Subsemigroup M
closure
(S :
Set: Type ?u.19642 โ†’ Type ?u.19642
Set
M: Type ?u.19606
M
) = S := (
Subsemigroup.gi: (M : Type ?u.19745) โ†’ [inst : Mul M] โ†’ GaloisInsertion closure SetLike.coe
Subsemigroup.gi
M: Type ?u.19606
M
).
l_u_eq: โˆ€ {ฮฑ : Type ?u.19754} {ฮฒ : Type ?u.19753} {l : ฮฑ โ†’ ฮฒ} {u : ฮฒ โ†’ ฮฑ} [inst : Preorder ฮฑ] [inst_1 : PartialOrder ฮฒ], GaloisInsertion l u โ†’ โˆ€ (b : ฮฒ), l (u b) = b
l_u_eq
S #align subsemigroup.closure_eq
Subsemigroup.closure_eq: โˆ€ {M : Type u_1} [inst : Mul M] (S : Subsemigroup M), closure โ†‘S = S
Subsemigroup.closure_eq
#align add_subsemigroup.closure_eq
AddSubsemigroup.closure_eq: โˆ€ {M : Type u_1} [inst : Add M] (S : AddSubsemigroup M), AddSubsemigroup.closure โ†‘S = S
AddSubsemigroup.closure_eq
@[
to_additive: โˆ€ {M : Type u_1} [inst : Add M], AddSubsemigroup.closure โˆ… = โŠฅ
to_additive
(attr := simp)] theorem
closure_empty: โˆ€ {M : Type u_1} [inst : Mul M], closure โˆ… = โŠฅ
closure_empty
:
closure: {M : Type ?u.19930} โ†’ [inst : Mul M] โ†’ Set M โ†’ Subsemigroup M
closure
(
โˆ…: ?m.19936
โˆ…
:
Set: Type ?u.19934 โ†’ Type ?u.19934
Set
M: Type ?u.19898
M
) =
โŠฅ: ?m.19986
โŠฅ
:= (
Subsemigroup.gi: (M : Type ?u.20044) โ†’ [inst : Mul M] โ†’ GaloisInsertion closure SetLike.coe
Subsemigroup.gi
M: Type ?u.19898
M
).
gc: โˆ€ {ฮฑ : Type ?u.20053} {ฮฒ : Type ?u.20052} [inst : Preorder ฮฑ] [inst_1 : Preorder ฮฒ] {l : ฮฑ โ†’ ฮฒ} {u : ฮฒ โ†’ ฮฑ}, GaloisInsertion l u โ†’ GaloisConnection l u
gc
.
l_bot: โˆ€ {ฮฑ : Type ?u.20142} {ฮฒ : Type ?u.20141} [inst : Preorder ฮฑ] [inst_1 : PartialOrder ฮฒ] [inst_2 : OrderBot ฮฒ] [inst_3 : OrderBot ฮฑ] {l : ฮฑ โ†’ ฮฒ} {u : ฮฒ โ†’ ฮฑ}, GaloisConnection l u โ†’ l โŠฅ = โŠฅ
l_bot
#align subsemigroup.closure_empty
Subsemigroup.closure_empty: โˆ€ {M : Type u_1} [inst : Mul M], closure โˆ… = โŠฅ
Subsemigroup.closure_empty
#align add_subsemigroup.closure_empty
AddSubsemigroup.closure_empty: โˆ€ {M : Type u_1} [inst : Add M], AddSubsemigroup.closure โˆ… = โŠฅ
AddSubsemigroup.closure_empty
@[
to_additive: โˆ€ {M : Type u_1} [inst : Add M], AddSubsemigroup.closure univ = โŠค
to_additive
(attr := simp)] theorem
closure_univ: closure univ = โŠค
closure_univ
:
closure: {M : Type ?u.20320} โ†’ [inst : Mul M] โ†’ Set M โ†’ Subsemigroup M
closure
(
univ: {ฮฑ : Type ?u.20325} โ†’ Set ฮฑ
univ
:
Set: Type ?u.20324 โ†’ Type ?u.20324
Set
M: Type ?u.20288
M
) =
โŠค: ?m.20336
โŠค
:= @
coe_top: โˆ€ {M : Type ?u.20385} [inst : Mul M], โ†‘โŠค = univ
coe_top
M: Type ?u.20288
M
_ โ–ธ
closure_eq: โˆ€ {M : Type ?u.20393} [inst : Mul M] (S : Subsemigroup M), closure โ†‘S = S
closure_eq
โŠค: ?m.20397
โŠค
#align subsemigroup.closure_univ
Subsemigroup.closure_univ: โˆ€ {M : Type u_1} [inst : Mul M], closure univ = โŠค
Subsemigroup.closure_univ
#align add_subsemigroup.closure_univ
AddSubsemigroup.closure_univ: โˆ€ {M : Type u_1} [inst : Add M], AddSubsemigroup.closure univ = โŠค
AddSubsemigroup.closure_univ
@[
to_additive: โˆ€ {M : Type u_1} [inst : Add M] (s t : Set M), AddSubsemigroup.closure (s โˆช t) = AddSubsemigroup.closure s โŠ” AddSubsemigroup.closure t
to_additive
] theorem
closure_union: โˆ€ (s t : Set M), closure (s โˆช t) = closure s โŠ” closure t
closure_union
(
s: Set M
s
t: Set M
t
:
Set: Type ?u.20523 โ†’ Type ?u.20523
Set
M: Type ?u.20489
M
) :
closure: {M : Type ?u.20527} โ†’ [inst : Mul M] โ†’ Set M โ†’ Subsemigroup M
closure
(
s: Set M
s
โˆช
t: Set M
t
) =
closure: {M : Type ?u.20558} โ†’ [inst : Mul M] โ†’ Set M โ†’ Subsemigroup M
closure
s: Set M
s
โŠ”
closure: {M : Type ?u.20576} โ†’ [inst : Mul M] โ†’ Set M โ†’ Subsemigroup M
closure
t: Set M
t
:= (
Subsemigroup.gi: (M : Type ?u.20626) โ†’ [inst : Mul M] โ†’ GaloisInsertion closure SetLike.coe
Subsemigroup.gi
M: Type ?u.20489
M
).
gc: โˆ€ {ฮฑ : Type ?u.20635} {ฮฒ : Type ?u.20634} [inst : Preorder ฮฑ] [inst_1 : Preorder ฮฒ] {l : ฮฑ โ†’ ฮฒ} {u : ฮฒ โ†’ ฮฑ}, GaloisInsertion l u โ†’ GaloisConnection l u
gc
.
l_sup: โˆ€ {ฮฑ : Type ?u.20724} {ฮฒ : Type ?u.20723} {aโ‚ aโ‚‚ : ฮฑ} [inst : SemilatticeSup ฮฑ] [inst_1 : SemilatticeSup ฮฒ] {l : ฮฑ โ†’ ฮฒ} {u : ฮฒ โ†’ ฮฑ}, GaloisConnection l u โ†’ l (aโ‚ โŠ” aโ‚‚) = l aโ‚ โŠ” l aโ‚‚
l_sup
#align subsemigroup.closure_union
Subsemigroup.closure_union: โˆ€ {M : Type u_1} [inst : Mul M] (s t : Set M), closure (s โˆช t) = closure s โŠ” closure t
Subsemigroup.closure_union
#align add_subsemigroup.closure_union
AddSubsemigroup.closure_union: โˆ€ {M : Type u_1} [inst : Add M] (s t : Set M), AddSubsemigroup.closure (s โˆช t) = AddSubsemigroup.closure s โŠ” AddSubsemigroup.closure t
AddSubsemigroup.closure_union
@[
to_additive: โˆ€ {M : Type u_2} [inst : Add M] {ฮน : Sort u_1} (s : ฮน โ†’ Set M), AddSubsemigroup.closure (iUnion fun i => s i) = โจ† i, AddSubsemigroup.closure (s i)
to_additive
] theorem
closure_iUnion: โˆ€ {M : Type u_2} [inst : Mul M] {ฮน : Sort u_1} (s : ฮน โ†’ Set M), closure (iUnion fun i => s i) = โจ† i, closure (s i)
closure_iUnion
{
ฮน: Sort u_1
ฮน
} (
s: ฮน โ†’ Set M
s
:
ฮน: ?m.20861
ฮน
โ†’
Set: Type ?u.20866 โ†’ Type ?u.20866
Set
M: Type ?u.20830
M
) :
closure: {M : Type ?u.20871} โ†’ [inst : Mul M] โ†’ Set M โ†’ Subsemigroup M
closure
(โ‹ƒ
i: ?m.20881
i
,
s: ฮน โ†’ Set M
s
i: ?m.20881
i
) = โจ†
i: ?m.20902
i
,
closure: {M : Type ?u.20904} โ†’ [inst : Mul M] โ†’ Set M โ†’ Subsemigroup M
closure
(
s: ฮน โ†’ Set M
s
i: ?m.20902
i
) := (
Subsemigroup.gi: (M : Type ?u.20953) โ†’ [inst : Mul M] โ†’ GaloisInsertion closure SetLike.coe
Subsemigroup.gi
M: Type ?u.20830
M
).
gc: โˆ€ {ฮฑ : Type ?u.20962} {ฮฒ : Type ?u.20961} [inst : Preorder ฮฑ] [inst_1 : Preorder ฮฒ] {l : ฮฑ โ†’ ฮฒ} {u : ฮฒ โ†’ ฮฑ}, GaloisInsertion l u โ†’ GaloisConnection l u
gc
.
l_iSup: โˆ€ {ฮฑ : Type ?u.21052} {ฮฒ : Type ?u.21051} {ฮน : Sort ?u.21050} [inst : CompleteLattice ฮฑ] [inst_1 : CompleteLattice ฮฒ] {l : ฮฑ โ†’ ฮฒ} {u : ฮฒ โ†’ ฮฑ}, GaloisConnection l u โ†’ โˆ€ {f : ฮน โ†’ ฮฑ}, l (iSup f) = โจ† i, l (f i)
l_iSup
#align subsemigroup.closure_Union
Subsemigroup.closure_iUnion: โˆ€ {M : Type u_2} [inst : Mul M] {ฮน : Sort u_1} (s : ฮน โ†’ Set M), closure (iUnion fun i => s i) = โจ† i, closure (s i)
Subsemigroup.closure_iUnion
#align add_subsemigroup.closure_Union
AddSubsemigroup.closure_iUnion: โˆ€ {M : Type u_2} [inst : Add M] {ฮน : Sort u_1} (s : ฮน โ†’ Set M), AddSubsemigroup.closure (iUnion fun i => s i) = โจ† i, AddSubsemigroup.closure (s i)
AddSubsemigroup.closure_iUnion
@[
to_additive: โˆ€ {M : Type u_1} [inst : Add M] (m : M) (p : AddSubsemigroup M), AddSubsemigroup.closure {m} โ‰ค p โ†” m โˆˆ p
to_additive
] theorem
closure_singleton_le_iff_mem: โˆ€ (m : M) (p : Subsemigroup M), closure {m} โ‰ค p โ†” m โˆˆ p
closure_singleton_le_iff_mem
(
m: M
m
:
M: Type ?u.21166
M
) (p :
Subsemigroup: (M : Type ?u.21199) โ†’ [inst : Mul M] โ†’ Type ?u.21199
Subsemigroup
M: Type ?u.21166
M
) :
closure: {M : Type ?u.21210} โ†’ [inst : Mul M] โ†’ Set M โ†’ Subsemigroup M
closure
{
m: M
m
} โ‰ค p โ†”
m: M
m
โˆˆ p :=

Goals accomplished! ๐Ÿ™
M: Type u_1

N: Type ?u.21169

A: Type ?u.21172

instโœยน: Mul M

s: Set M

instโœ: Add A

t: Set A

S: Subsemigroup M

m: M

p: Subsemigroup M


M: Type u_1

N: Type ?u.21169

A: Type ?u.21172

instโœยน: Mul M

s: Set M

instโœ: Add A

t: Set A

S: Subsemigroup M

m: M

p: Subsemigroup M


M: Type u_1

N: Type ?u.21169

A: Type ?u.21172

instโœยน: Mul M

s: Set M

instโœ: Add A

t: Set A

S: Subsemigroup M

m: M

p: Subsemigroup M


{m} โŠ† โ†‘p โ†” m โˆˆ p
M: Type u_1

N: Type ?u.21169

A: Type ?u.21172

instโœยน: Mul M

s: Set M

instโœ: Add A

t: Set A

S: Subsemigroup M

m: M

p: Subsemigroup M


M: Type u_1

N: Type ?u.21169

A: Type ?u.21172

instโœยน: Mul M

s: Set M

instโœ: Add A

t: Set A

S: Subsemigroup M

m: M

p: Subsemigroup M


m โˆˆ โ†‘p โ†” m โˆˆ p
M: Type u_1

N: Type ?u.21169

A: Type ?u.21172

instโœยน: Mul M

s: Set M

instโœ: Add A

t: Set A

S: Subsemigroup M

m: M

p: Subsemigroup M


M: Type u_1

N: Type ?u.21169

A: Type ?u.21172

instโœยน: Mul M

s: Set M

instโœ: Add A

t: Set A

S: Subsemigroup M

m: M

p: Subsemigroup M



Goals accomplished! ๐Ÿ™
#align subsemigroup.closure_singleton_le_iff_mem
Subsemigroup.closure_singleton_le_iff_mem: โˆ€ {M : Type u_1} [inst : Mul M] (m : M) (p : Subsemigroup M), closure {m} โ‰ค p โ†” m โˆˆ p
Subsemigroup.closure_singleton_le_iff_mem
#align add_subsemigroup.closure_singleton_le_iff_mem
AddSubsemigroup.closure_singleton_le_iff_mem: โˆ€ {M : Type u_1} [inst : Add M] (m : M) (p : AddSubsemigroup M), AddSubsemigroup.closure {m} โ‰ค p โ†” m โˆˆ p
AddSubsemigroup.closure_singleton_le_iff_mem
@[
to_additive: โˆ€ {M : Type u_2} [inst : Add M] {ฮน : Sort u_1} (p : ฮน โ†’ AddSubsemigroup M) {m : M}, (m โˆˆ โจ† i, p i) โ†” โˆ€ (N : AddSubsemigroup M), (โˆ€ (i : ฮน), p i โ‰ค N) โ†’ m โˆˆ N
to_additive
] theorem
mem_iSup: โˆ€ {ฮน : Sort u_1} (p : ฮน โ†’ Subsemigroup M) {m : M}, (m โˆˆ โจ† i, p i) โ†” โˆ€ (N : Subsemigroup M), (โˆ€ (i : ฮน), p i โ‰ค N) โ†’ m โˆˆ N
mem_iSup
{
ฮน: Sort u_1
ฮน
:
Sort _: Type ?u.21487
Sort
Sort _: Type ?u.21487
_
} (
p: ฮน โ†’ Subsemigroup M
p
:
ฮน: Sort ?u.21487
ฮน
โ†’
Subsemigroup: (M : Type ?u.21492) โ†’ [inst : Mul M] โ†’ Type ?u.21492
Subsemigroup
M: Type ?u.21456
M
) {
m: M
m
:
M: Type ?u.21456
M
} : (
m: M
m
โˆˆ โจ†
i: ?m.21527
i
,
p: ฮน โ†’ Subsemigroup M
p
i: ?m.21527
i
) โ†” โˆ€
N: ?m.21573
N
, (โˆ€
i: ?m.21578
i
,
p: ฮน โ†’ Subsemigroup M
p
i: ?m.21578
i
โ‰ค
N: ?m.21573
N
) โ†’
m: M
m
โˆˆ
N: ?m.21573
N
:=

Goals accomplished! ๐Ÿ™
M: Type u_2

N: Type ?u.21459

A: Type ?u.21462

instโœยน: Mul M

s: Set M

instโœ: Add A

t: Set A

S: Subsemigroup M

ฮน: Sort u_1

p: ฮน โ†’ Subsemigroup M

m: M


(m โˆˆ โจ† i, p i) โ†” โˆ€ (N : Subsemigroup M), (โˆ€ (i : ฮน), p i โ‰ค N) โ†’ m โˆˆ N
M: Type u_2

N: Type ?u.21459

A: Type ?u.21462

instโœยน: Mul M

s: Set M

instโœ: Add A

t: Set A

S: Subsemigroup M

ฮน: Sort u_1

p: ฮน โ†’ Subsemigroup M

m: M


(m โˆˆ โจ† i, p i) โ†” โˆ€ (N : Subsemigroup M), (โˆ€ (i : ฮน), p i โ‰ค N) โ†’ m โˆˆ N
M: Type u_2

N: Type ?u.21459

A: Type ?u.21462

instโœยน: Mul M

s: Set M

instโœ: Add A

t: Set A

S: Subsemigroup M

ฮน: Sort u_1

p: ฮน โ†’ Subsemigroup M

m: M


(closure {m} โ‰ค โจ† i, p i) โ†” โˆ€ (N : Subsemigroup M), (โˆ€ (i : ฮน), p i โ‰ค N) โ†’ m โˆˆ N
M: Type u_2

N: Type ?u.21459

A: Type ?u.21462

instโœยน: Mul M

s: Set M

instโœ: Add A

t: Set A

S: Subsemigroup M

ฮน: Sort u_1

p: ฮน โ†’ Subsemigroup M

m: M


(m โˆˆ โจ† i, p i) โ†” โˆ€ (N : Subsemigroup M), (โˆ€ (i : ฮน), p i โ‰ค N) โ†’ m โˆˆ N
M: Type u_2

N: Type ?u.21459

A: Type ?u.21462

instโœยน: Mul M

s: Set M

instโœ: Add A

t: Set A

S: Subsemigroup M

ฮน: Sort u_1

p: ฮน โ†’ Subsemigroup M

m: M


(โˆ€ (b : Subsemigroup M), (โˆ€ (i : ฮน), p i โ‰ค b) โ†’ closure {m} โ‰ค b) โ†” โˆ€ (N : Subsemigroup M), (โˆ€ (i : ฮน), p i โ‰ค N) โ†’ m โˆˆ N
M: Type u_2

N: Type ?u.21459

A: Type ?u.21462

instโœยน: Mul M

s: Set M

instโœ: Add A

t: Set A

S: Subsemigroup M

ฮน: Sort u_1

p: ฮน โ†’ Subsemigroup M

m: M


(โˆ€ (b : Subsemigroup M), (โˆ€ (i : ฮน), p i โ‰ค b) โ†’ closure {m} โ‰ค b) โ†” โˆ€ (N : Subsemigroup M), (โˆ€ (i : ฮน), p i โ‰ค N) โ†’ m โˆˆ N
M: Type u_2

N: Type ?u.21459

A: Type ?u.21462

instโœยน: Mul M

s: Set M

instโœ: Add A

t: Set A

S: Subsemigroup M

ฮน: Sort u_1

p: ฮน โ†’ Subsemigroup M

m: M


(m โˆˆ โจ† i, p i) โ†” โˆ€ (N : Subsemigroup M), (โˆ€ (i : ฮน), p i โ‰ค N) โ†’ m โˆˆ N

Goals accomplished! ๐Ÿ™
#align subsemigroup.mem_supr
Subsemigroup.mem_iSup: โˆ€ {M : Type u_2} [inst : Mul M] {ฮน : Sort u_1} (p : ฮน โ†’ Subsemigroup M) {m : M}, (m โˆˆ โจ† i, p i) โ†” โˆ€ (N : Subsemigroup M), (โˆ€ (i : ฮน), p i โ‰ค N) โ†’ m โˆˆ N
Subsemigroup.mem_iSup
#align add_subsemigroup.mem_supr
AddSubsemigroup.mem_iSup: โˆ€ {M : Type u_2} [inst : Add M] {ฮน : Sort u_1} (p : ฮน โ†’ AddSubsemigroup M) {m : M}, (m โˆˆ โจ† i, p i) โ†” โˆ€ (N : AddSubsemigroup M), (โˆ€ (i : ฮน), p i โ‰ค N) โ†’ m โˆˆ N
AddSubsemigroup.mem_iSup
@[
to_additive: โˆ€ {M : Type u_2} [inst : Add M] {ฮน : Sort u_1} (p : ฮน โ†’ AddSubsemigroup M), (โจ† i, p i) = AddSubsemigroup.closure (iUnion fun i => โ†‘(p i))
to_additive
] theorem
iSup_eq_closure: โˆ€ {ฮน : Sort u_1} (p : ฮน โ†’ Subsemigroup M), (โจ† i, p i) = closure (iUnion fun i => โ†‘(p i))
iSup_eq_closure
{
ฮน: Sort u_1
ฮน
:
Sort _: Type ?u.22198
Sort
Sort _: Type ?u.22198
_
} (
p: ฮน โ†’ Subsemigroup M
p
:
ฮน: Sort ?u.22198
ฮน
โ†’
Subsemigroup: (M : Type ?u.22203) โ†’ [inst : Mul M] โ†’ Type ?u.22203
Subsemigroup
M: Type ?u.22167
M
) : (โจ†
i: ?m.22220
i
,
p: ฮน โ†’ Subsemigroup M
p
i: ?m.22220
i
) =
Subsemigroup.closure: {M : Type ?u.22247} โ†’ [inst : Mul M] โ†’ Set M โ†’ Subsemigroup M
Subsemigroup.closure
(โ‹ƒ
i: ?m.22257
i
, (
p: ฮน โ†’ Subsemigroup M
p
i: ?m.22257
i
:
Set: Type ?u.22260 โ†’ Type ?u.22260
Set
M: Type ?u.22167
M
)) :=

Goals accomplished! ๐Ÿ™
M: Type u_2

N: Type ?u.22170

A: Type ?u.22173

instโœยน: Mul M

s: Set M

instโœ: Add A

t: Set A

S: Subsemigroup M

ฮน: Sort u_1

p: ฮน โ†’ Subsemigroup M


(โจ† i, p i) = closure (iUnion fun i => โ†‘(p i))
M: Type u_2

N: Type ?u.22170

A: Type ?u.22173

instโœยน: Mul M

s: Set M

instโœ: Add A

t: Set A

S: Subsemigroup M

ฮน: Sort u_1

p: ฮน โ†’ Subsemigroup M


(โจ† i, p i) = closure (iUnion fun i => โ†‘(p i))
M: Type u_2

N: Type ?u.22170

A: Type ?u.22173

instโœยน: Mul M

s: Set M

instโœ: Add A

t: Set A

S: Subsemigroup M

ฮน: Sort u_1

p: ฮน โ†’ Subsemigroup M


(โจ† i, p i) = โจ† i, closure โ†‘(p i)